; benchmark generated from python API
(set-info :status unknown)
(declare-fun rec_tbl_kid_24_feasible () Bool)
(declare-fun rec_tbl_kid_23_feasible () Bool)
(declare-fun rec_tbl_kid_22_feasible () Bool)
(declare-fun rec_tbl_kid_21_feasible () Bool)
(declare-fun rec_tbl_kid_20_feasible () Bool)
(declare-fun rec_tbl_kid_19_feasible () Bool)
(declare-fun rec_tbl_kid_18_feasible () Bool)
(declare-fun rec_tbl_kid_17_feasible () Bool)
(declare-fun rec_tbl_kid_16_feasible () Bool)
(declare-fun rec_tbl_kid_15_feasible () Bool)
(declare-fun rec_tbl_kid_14_feasible () Bool)
(declare-fun rec_tbl_kid_13_feasible () Bool)
(declare-fun rec_tbl_kid_12_feasible () Bool)
(declare-fun rec_tbl_kid_11_feasible () Bool)
(declare-fun rec_tbl_kid_10_feasible () Bool)
(declare-fun rec_tbl_kid_9_feasible () Bool)
(declare-fun rec_tbl_kid_8_feasible () Bool)
(declare-fun rec_tbl_kid_7_feasible () Bool)
(declare-fun rec_tbl_kid_6_feasible () Bool)
(declare-fun rec_tbl_kid_5_feasible () Bool)
(declare-fun rec_tbl_kid_4_feasible () Bool)
(declare-fun rec_tbl_kid_3_feasible () Bool)
(declare-fun rec_tbl_kid_2_feasible () Bool)
(declare-fun rec_tbl_kid_1_feasible () Bool)
(declare-fun rec_tbl_kid_0_feasible () Bool)
(declare-fun select_kid_5_feasible () Bool)
(declare-fun select_kid_4_feasible () Bool)
(declare-fun select_kid_3_feasible () Bool)
(declare-fun select_kid_2_feasible () Bool)
(declare-fun select_kid_1_feasible () Bool)
(declare-fun select_kid_0_feasible () Bool)
(declare-fun rec_tbl_feasible () Bool)
(declare-fun select_feasible () Bool)
(declare-fun rec_title_feasible () Bool)
(declare-fun welcome_kid_3_kid_4_feasible () Bool)
(declare-fun welcome_kid_3_feasible () Bool)
(declare-fun welcome_kid_3_kid_3_feasible () Bool)
(declare-fun welcome_kid_3_kid_2_feasible () Bool)
(declare-fun welcome_kid_3_kid_1_feasible () Bool)
(declare-fun welcome_kid_3_kid_0_feasible () Bool)
(declare-fun welcome_kid_2_kid_5_feasible () Bool)
(declare-fun welcome_kid_2_feasible () Bool)
(declare-fun welcome_kid_2_kid_4_feasible () Bool)
(declare-fun welcome_kid_2_kid_3_feasible () Bool)
(declare-fun welcome_kid_2_kid_2_feasible () Bool)
(declare-fun welcome_kid_2_kid_1_feasible () Bool)
(declare-fun welcome_kid_2_kid_0_feasible () Bool)
(declare-fun welcome_kid_1_kid_5_feasible () Bool)
(declare-fun welcome_kid_1_feasible () Bool)
(declare-fun welcome_kid_1_kid_4_feasible () Bool)
(declare-fun welcome_kid_1_kid_3_feasible () Bool)
(declare-fun welcome_kid_1_kid_2_feasible () Bool)
(declare-fun welcome_kid_1_kid_1_feasible () Bool)
(declare-fun welcome_kid_1_kid_0_feasible () Bool)
(declare-fun welcome_kid_0_kid_2_feasible () Bool)
(declare-fun welcome_kid_0_feasible () Bool)
(declare-fun welcome_kid_0_kid_1_feasible () Bool)
(declare-fun welcome_kid_0_kid_0_feasible () Bool)
(declare-fun welcome_feasible () Bool)
(declare-fun ads2_feasible () Bool)
(declare-fun ads_feasible () Bool)
(declare-fun pic_feasible () Bool)
(declare-fun side_bar_feasible () Bool)
(declare-fun recommend_feasible () Bool)
(declare-fun ads_holder_feasible () Bool)
(declare-fun cart_feasible () Bool)
(declare-fun search_icon_feasible () Bool)
(declare-fun search_box_feasible () Bool)
(declare-fun search_buttons_kid_5_feasible () Bool)
(declare-fun search_buttons_kid_4_feasible () Bool)
(declare-fun search_buttons_kid_3_feasible () Bool)
(declare-fun search_buttons_kid_2_feasible () Bool)
(declare-fun search_buttons_kid_1_feasible () Bool)
(declare-fun search_buttons_kid_0_feasible () Bool)
(declare-fun search_buttons_feasible () Bool)
(declare-fun icon_feasible () Bool)
(declare-fun title_top_right_kid_7_feasible () Bool)
(declare-fun title_top_right_kid_6_feasible () Bool)
(declare-fun title_top_right_kid_5_feasible () Bool)
(declare-fun title_top_right_kid_4_feasible () Bool)
(declare-fun title_top_right_kid_3_feasible () Bool)
(declare-fun title_top_right_kid_2_feasible () Bool)
(declare-fun title_top_right_kid_1_feasible () Bool)
(declare-fun title_top_right_kid_0_feasible () Bool)
(declare-fun title_top_left_kid_2_feasible () Bool)
(declare-fun title_top_left_kid_1_feasible () Bool)
(declare-fun title_top_left_kid_0_feasible () Bool)
(declare-fun title_top_right_feasible () Bool)
(declare-fun title_top_left_feasible () Bool)
(declare-fun title_bar_feasible () Bool)
(declare-fun title_top_feasible () Bool)
(declare-fun main_body_feasible () Bool)
(declare-fun title_bg_feasible () Bool)
(declare-fun back_ground_feasible () Bool)
(declare-fun rec_tbl_kid_24_hight () Real)
(declare-fun rec_tbl_kid_24_width () Real)
(declare-fun rec_tbl_kid_23_hight () Real)
(declare-fun rec_tbl_kid_23_width () Real)
(declare-fun rec_tbl_kid_22_width () Real)
(declare-fun rec_tbl_kid_22_hight () Real)
(declare-fun rec_tbl_kid_21_width () Real)
(declare-fun rec_tbl_kid_21_hight () Real)
(declare-fun rec_tbl_kid_20_width () Real)
(declare-fun rec_tbl_kid_20_hight () Real)
(declare-fun rec_tbl_kid_19_width () Real)
(declare-fun rec_tbl_kid_19_hight () Real)
(declare-fun rec_tbl_kid_18_width () Real)
(declare-fun rec_tbl_kid_18_hight () Real)
(declare-fun rec_tbl_kid_17_hight () Real)
(declare-fun rec_tbl_kid_17_width () Real)
(declare-fun rec_tbl_kid_16_width () Real)
(declare-fun rec_tbl_kid_16_hight () Real)
(declare-fun rec_tbl_kid_15_width () Real)
(declare-fun rec_tbl_kid_15_hight () Real)
(declare-fun rec_tbl_kid_14_width () Real)
(declare-fun rec_tbl_kid_14_hight () Real)
(declare-fun rec_tbl_kid_13_width () Real)
(declare-fun rec_tbl_kid_13_hight () Real)
(declare-fun rec_tbl_kid_12_width () Real)
(declare-fun rec_tbl_kid_12_hight () Real)
(declare-fun rec_tbl_kid_11_hight () Real)
(declare-fun rec_tbl_kid_11_width () Real)
(declare-fun rec_tbl_kid_10_hight () Real)
(declare-fun rec_tbl_kid_10_width () Real)
(declare-fun rec_tbl_kid_9_width () Real)
(declare-fun rec_tbl_kid_9_hight () Real)
(declare-fun rec_tbl_kid_8_width () Real)
(declare-fun rec_tbl_kid_8_hight () Real)
(declare-fun rec_tbl_kid_7_width () Real)
(declare-fun rec_tbl_kid_7_hight () Real)
(declare-fun rec_tbl_kid_6_width () Real)
(declare-fun rec_tbl_kid_6_hight () Real)
(declare-fun rec_tbl_kid_5_hight () Real)
(declare-fun rec_tbl_kid_5_width () Real)
(declare-fun rec_tbl_kid_4_hight () Real)
(declare-fun rec_tbl_kid_4_width () Real)
(declare-fun rec_tbl_kid_3_hight () Real)
(declare-fun rec_tbl_kid_3_width () Real)
(declare-fun rec_tbl_kid_2_width () Real)
(declare-fun rec_tbl_kid_2_hight () Real)
(declare-fun rec_tbl_kid_1_width () Real)
(declare-fun rec_tbl_kid_1_hight () Real)
(declare-fun rec_tbl_kid_0_width () Real)
(declare-fun rec_tbl_kid_0_hight () Real)
(declare-fun rec_tbl_kid_20_y () Real)
(declare-fun rec_tbl_kid_15_y () Real)
(declare-fun rec_tbl_kid_10_y () Real)
(declare-fun rec_tbl_kid_5_y () Real)
(declare-fun rec_tbl_kid_0_y () Real)
(declare-fun rec_tbl_kid_4_x () Real)
(declare-fun rec_tbl_kid_3_x () Real)
(declare-fun rec_tbl_kid_2_x () Real)
(declare-fun rec_tbl_kid_1_x () Real)
(declare-fun rec_tbl_kid_0_x () Real)
(declare-fun rec_tbl_kid_24_x () Real)
(declare-fun rec_tbl_kid_19_x () Real)
(declare-fun rec_tbl_kid_14_x () Real)
(declare-fun rec_tbl_kid_9_x () Real)
(declare-fun rec_tbl_kid_23_x () Real)
(declare-fun rec_tbl_kid_18_x () Real)
(declare-fun rec_tbl_kid_13_x () Real)
(declare-fun rec_tbl_kid_8_x () Real)
(declare-fun rec_tbl_kid_22_x () Real)
(declare-fun rec_tbl_kid_17_x () Real)
(declare-fun rec_tbl_kid_12_x () Real)
(declare-fun rec_tbl_kid_7_x () Real)
(declare-fun rec_tbl_kid_21_x () Real)
(declare-fun rec_tbl_kid_16_x () Real)
(declare-fun rec_tbl_kid_11_x () Real)
(declare-fun rec_tbl_kid_6_x () Real)
(declare-fun rec_tbl_kid_20_x () Real)
(declare-fun rec_tbl_kid_15_x () Real)
(declare-fun rec_tbl_kid_10_x () Real)
(declare-fun rec_tbl_kid_5_x () Real)
(declare-fun rec_tbl_kid_24_y () Real)
(declare-fun rec_tbl_kid_23_y () Real)
(declare-fun rec_tbl_kid_22_y () Real)
(declare-fun rec_tbl_kid_21_y () Real)
(declare-fun rec_tbl_kid_19_y () Real)
(declare-fun rec_tbl_kid_18_y () Real)
(declare-fun rec_tbl_kid_17_y () Real)
(declare-fun rec_tbl_kid_16_y () Real)
(declare-fun rec_tbl_kid_14_y () Real)
(declare-fun rec_tbl_kid_13_y () Real)
(declare-fun rec_tbl_kid_12_y () Real)
(declare-fun rec_tbl_kid_11_y () Real)
(declare-fun rec_tbl_kid_9_y () Real)
(declare-fun rec_tbl_kid_8_y () Real)
(declare-fun rec_tbl_kid_7_y () Real)
(declare-fun rec_tbl_kid_6_y () Real)
(declare-fun rec_tbl_kid_4_y () Real)
(declare-fun rec_tbl_kid_3_y () Real)
(declare-fun rec_tbl_kid_2_y () Real)
(declare-fun rec_tbl_kid_1_y () Real)
(declare-fun rec_tbl_hight () Real)
(declare-fun rec_tbl_y () Real)
(declare-fun rec_tbl_width () Real)
(declare-fun rec_tbl_x () Real)
(declare-fun recommend_width () Real)
(declare-fun recommend_x () Real)
(declare-fun select_kid_4_x () Real)
(declare-fun select_kid_5_x () Real)
(declare-fun select_kid_4_width () Real)
(declare-fun select_kid_3_x () Real)
(declare-fun select_kid_3_width () Real)
(declare-fun select_kid_2_x () Real)
(declare-fun select_kid_2_width () Real)
(declare-fun select_kid_1_width () Real)
(declare-fun select_kid_1_x () Real)
(declare-fun select_kid_0_width () Real)
(declare-fun select_kid_0_x () Real)
(declare-fun select_kid_5_width () Real)
(declare-fun select_hight () Real)
(declare-fun select_width () Real)
(declare-fun select_x () Real)
(declare-fun select_kid_5_hight () Real)
(declare-fun select_y () Real)
(declare-fun select_kid_5_y () Real)
(declare-fun select_kid_4_hight () Real)
(declare-fun select_kid_4_y () Real)
(declare-fun select_kid_3_hight () Real)
(declare-fun select_kid_3_y () Real)
(declare-fun select_kid_2_hight () Real)
(declare-fun select_kid_2_y () Real)
(declare-fun select_kid_1_y () Real)
(declare-fun select_kid_1_hight () Real)
(declare-fun select_kid_0_hight () Real)
(declare-fun select_kid_0_y () Real)
(declare-fun recommend_y () Real)
(declare-fun rec_title_y () Real)
(declare-fun rec_title_x () Real)
(declare-fun rec_title_width () Real)
(declare-fun rec_title_hight () Real)
(declare-fun recommend_hight () Real)
(declare-fun ads2_hight () Real)
(declare-fun ads2_y () Real)
(declare-fun welcome_hight () Real)
(declare-fun welcome_y () Real)
(declare-fun pic_hight () Real)
(declare-fun pic_y () Real)
(declare-fun ads2_x () Real)
(declare-fun welcome_width () Real)
(declare-fun welcome_x () Real)
(declare-fun pic_x () Real)
(declare-fun ads2_width () Real)
(declare-fun pic_width () Real)
(declare-fun welcome_kid_3_kid_0_width () Real)
(declare-fun welcome_kid_3_kid_4_width () Real)
(declare-fun welcome_kid_3_kid_3_width () Real)
(declare-fun welcome_kid_3_kid_2_width () Real)
(declare-fun welcome_kid_3_kid_1_width () Real)
(declare-fun welcome_kid_3_kid_4_x () Real)
(declare-fun welcome_kid_3_kid_3_x () Real)
(declare-fun welcome_kid_3_kid_2_x () Real)
(declare-fun welcome_kid_3_kid_1_x () Real)
(declare-fun welcome_kid_3_kid_0_x () Real)
(declare-fun welcome_kid_3_kid_4_hight () Real)
(declare-fun welcome_kid_3_kid_0_hight () Real)
(declare-fun welcome_kid_3_kid_4_y () Real)
(declare-fun welcome_kid_3_kid_0_y () Real)
(declare-fun welcome_kid_3_kid_3_hight () Real)
(declare-fun welcome_kid_3_kid_3_y () Real)
(declare-fun welcome_kid_3_kid_2_hight () Real)
(declare-fun welcome_kid_3_kid_2_y () Real)
(declare-fun welcome_kid_3_kid_1_hight () Real)
(declare-fun welcome_kid_3_kid_1_y () Real)
(declare-fun welcome_kid_3_hight () Real)
(declare-fun welcome_kid_3_y () Real)
(declare-fun welcome_kid_3_x () Real)
(declare-fun welcome_kid_3_width () Real)
(declare-fun welcome_kid_2_kid_4_x () Real)
(declare-fun welcome_kid_2_kid_0_width () Real)
(declare-fun welcome_kid_2_kid_5_x () Real)
(declare-fun welcome_kid_2_kid_0_x () Real)
(declare-fun welcome_kid_2_kid_1_x () Real)
(declare-fun welcome_kid_2_kid_4_width () Real)
(declare-fun welcome_kid_2_kid_3_width () Real)
(declare-fun welcome_kid_2_kid_3_x () Real)
(declare-fun welcome_kid_2_kid_2_width () Real)
(declare-fun welcome_kid_2_kid_2_x () Real)
(declare-fun welcome_kid_2_kid_1_width () Real)
(declare-fun welcome_kid_2_kid_5_width () Real)
(declare-fun welcome_kid_2_hight () Real)
(declare-fun welcome_kid_2_y () Real)
(declare-fun welcome_kid_2_kid_5_hight () Real)
(declare-fun welcome_kid_2_kid_5_y () Real)
(declare-fun welcome_kid_2_kid_4_hight () Real)
(declare-fun welcome_kid_2_kid_4_y () Real)
(declare-fun welcome_kid_2_kid_3_hight () Real)
(declare-fun welcome_kid_2_kid_3_y () Real)
(declare-fun welcome_kid_2_kid_2_hight () Real)
(declare-fun welcome_kid_2_kid_2_y () Real)
(declare-fun welcome_kid_2_kid_1_y () Real)
(declare-fun welcome_kid_2_kid_1_hight () Real)
(declare-fun welcome_kid_2_kid_0_hight () Real)
(declare-fun welcome_kid_2_kid_0_y () Real)
(declare-fun welcome_kid_2_width () Real)
(declare-fun welcome_kid_2_x () Real)
(declare-fun welcome_kid_1_kid_4_width () Real)
(declare-fun welcome_kid_1_kid_4_x () Real)
(declare-fun welcome_kid_1_kid_0_width () Real)
(declare-fun welcome_kid_1_kid_5_x () Real)
(declare-fun welcome_kid_1_kid_0_x () Real)
(declare-fun welcome_kid_1_kid_1_x () Real)
(declare-fun welcome_kid_1_kid_3_x () Real)
(declare-fun welcome_kid_1_kid_3_width () Real)
(declare-fun welcome_kid_1_kid_2_width () Real)
(declare-fun welcome_kid_1_kid_2_x () Real)
(declare-fun welcome_kid_1_kid_1_width () Real)
(declare-fun welcome_kid_1_kid_5_width () Real)
(declare-fun welcome_kid_1_hight () Real)
(declare-fun welcome_kid_1_y () Real)
(declare-fun welcome_kid_1_kid_5_hight () Real)
(declare-fun welcome_kid_1_kid_5_y () Real)
(declare-fun welcome_kid_1_kid_4_hight () Real)
(declare-fun welcome_kid_1_kid_4_y () Real)
(declare-fun welcome_kid_1_kid_3_hight () Real)
(declare-fun welcome_kid_1_kid_3_y () Real)
(declare-fun welcome_kid_1_kid_2_y () Real)
(declare-fun welcome_kid_1_kid_2_hight () Real)
(declare-fun welcome_kid_1_kid_1_hight () Real)
(declare-fun welcome_kid_1_kid_1_y () Real)
(declare-fun welcome_kid_1_kid_0_y () Real)
(declare-fun welcome_kid_1_kid_0_hight () Real)
(declare-fun welcome_kid_1_width () Real)
(declare-fun welcome_kid_1_x () Real)
(declare-fun welcome_kid_0_kid_2_x () Real)
(declare-fun welcome_kid_0_kid_1_x () Real)
(declare-fun welcome_kid_0_kid_1_width () Real)
(declare-fun welcome_kid_0_kid_0_width () Real)
(declare-fun welcome_kid_0_kid_0_x () Real)
(declare-fun welcome_kid_0_y () Real)
(declare-fun welcome_kid_0_kid_2_hight () Real)
(declare-fun welcome_kid_0_kid_2_y () Real)
(declare-fun welcome_kid_0_hight () Real)
(declare-fun welcome_kid_0_kid_1_hight () Real)
(declare-fun welcome_kid_0_kid_1_y () Real)
(declare-fun welcome_kid_0_kid_0_hight () Real)
(declare-fun welcome_kid_0_kid_0_y () Real)
(declare-fun welcome_kid_0_kid_2_width () Real)
(declare-fun welcome_kid_0_width () Real)
(declare-fun welcome_kid_0_x () Real)
(declare-fun side_bar_width () Real)
(declare-fun ads_y () Real)
(declare-fun ads_hight () Real)
(declare-fun side_bar_hight () Real)
(declare-fun side_bar_y () Real)
(declare-fun ads_width () Real)
(declare-fun ads_x () Real)
(declare-fun side_bar_x () Real)
(declare-fun ads_holder_hight () Real)
(declare-fun ads_holder_y () Real)
(declare-fun ads_holder_width () Real)
(declare-fun ads_holder_x () Real)
(declare-fun main_body_width () Real)
(declare-fun back_ground_width () Real)
(declare-fun back_ground_x () Real)
(declare-fun main_body_x () Real)
(declare-fun main_body_hight () Real)
(declare-fun main_body_y () Real)
(declare-fun cart_width () Real)
(declare-fun cart_x () Real)
(declare-fun search_icon_x () Real)
(declare-fun search_icon_width () Real)
(declare-fun search_box_hight () Real)
(declare-fun cart_hight () Real)
(declare-fun search_box_y () Real)
(declare-fun cart_y () Real)
(declare-fun search_box_width () Real)
(declare-fun search_box_x () Real)
(declare-fun search_icon_hight () Real)
(declare-fun search_icon_y () Real)
(declare-fun title_bg_width () Real)
(declare-fun title_bg_x () Real)
(declare-fun title_bg_hight () Real)
(declare-fun title_bg_y () Real)
(declare-fun title_bar_hight () Real)
(declare-fun title_bar_y () Real)
(declare-fun search_buttons_hight () Real)
(declare-fun search_buttons_y () Real)
(declare-fun search_buttons_kid_5_x () Real)
(declare-fun search_buttons_kid_4_width () Real)
(declare-fun search_buttons_kid_4_x () Real)
(declare-fun search_buttons_kid_3_width () Real)
(declare-fun search_buttons_kid_3_x () Real)
(declare-fun search_buttons_kid_2_width () Real)
(declare-fun search_buttons_kid_2_x () Real)
(declare-fun search_buttons_kid_1_width () Real)
(declare-fun search_buttons_kid_1_x () Real)
(declare-fun search_buttons_kid_0_x () Real)
(declare-fun search_buttons_kid_0_width () Real)
(declare-fun search_buttons_kid_5_hight () Real)
(declare-fun search_buttons_kid_5_y () Real)
(declare-fun search_buttons_kid_4_y () Real)
(declare-fun search_buttons_kid_4_hight () Real)
(declare-fun search_buttons_kid_3_y () Real)
(declare-fun search_buttons_kid_3_hight () Real)
(declare-fun search_buttons_kid_2_hight () Real)
(declare-fun search_buttons_kid_2_y () Real)
(declare-fun search_buttons_kid_1_hight () Real)
(declare-fun search_buttons_kid_1_y () Real)
(declare-fun search_buttons_kid_0_hight () Real)
(declare-fun search_buttons_kid_0_y () Real)
(declare-fun search_buttons_x () Real)
(declare-fun search_buttons_kid_5_width () Real)
(declare-fun search_buttons_width () Real)
(declare-fun title_bar_x () Real)
(declare-fun icon_x () Real)
(declare-fun icon_hight () Real)
(declare-fun icon_y () Real)
(declare-fun icon_width () Real)
(declare-fun title_bar_width () Real)
(declare-fun title_top_right_x () Real)
(declare-fun title_top_width () Real)
(declare-fun title_top_x () Real)
(declare-fun title_top_right_width () Real)
(declare-fun title_top_left_x () Real)
(declare-fun title_top_right_kid_6_width () Real)
(declare-fun title_top_right_kid_7_x () Real)
(declare-fun title_top_right_kid_6_x () Real)
(declare-fun title_top_right_kid_5_width () Real)
(declare-fun title_top_right_kid_5_x () Real)
(declare-fun title_top_right_kid_4_width () Real)
(declare-fun title_top_right_kid_4_x () Real)
(declare-fun title_top_right_kid_3_x () Real)
(declare-fun title_top_right_kid_3_width () Real)
(declare-fun title_top_right_kid_2_x () Real)
(declare-fun title_top_right_kid_2_width () Real)
(declare-fun title_top_right_kid_1_width () Real)
(declare-fun title_top_right_kid_1_x () Real)
(declare-fun title_top_right_kid_0_width () Real)
(declare-fun title_top_right_kid_0_x () Real)
(declare-fun title_top_right_kid_7_y () Real)
(declare-fun title_top_right_hight () Real)
(declare-fun title_top_right_y () Real)
(declare-fun title_top_right_kid_7_hight () Real)
(declare-fun title_top_right_kid_6_y () Real)
(declare-fun title_top_right_kid_6_hight () Real)
(declare-fun title_top_right_kid_5_hight () Real)
(declare-fun title_top_right_kid_5_y () Real)
(declare-fun title_top_right_kid_4_hight () Real)
(declare-fun title_top_right_kid_4_y () Real)
(declare-fun title_top_right_kid_3_hight () Real)
(declare-fun title_top_right_kid_3_y () Real)
(declare-fun title_top_right_kid_2_hight () Real)
(declare-fun title_top_right_kid_2_y () Real)
(declare-fun title_top_right_kid_1_hight () Real)
(declare-fun title_top_right_kid_1_y () Real)
(declare-fun title_top_right_kid_0_y () Real)
(declare-fun title_top_right_kid_0_hight () Real)
(declare-fun title_top_right_kid_7_width () Real)
(declare-fun title_top_left_kid_2_y () Real)
(declare-fun title_top_left_hight () Real)
(declare-fun title_top_left_y () Real)
(declare-fun title_top_left_kid_2_hight () Real)
(declare-fun title_top_left_kid_1_hight () Real)
(declare-fun title_top_left_kid_1_y () Real)
(declare-fun title_top_left_kid_0_hight () Real)
(declare-fun title_top_left_kid_0_y () Real)
(declare-fun title_top_left_kid_2_width () Real)
(declare-fun title_top_left_kid_2_x () Real)
(declare-fun title_top_left_width () Real)
(declare-fun title_top_left_kid_0_x () Real)
(declare-fun title_top_left_kid_1_width () Real)
(declare-fun title_top_left_kid_0_width () Real)
(declare-fun title_top_left_kid_1_x () Real)
(declare-fun title_top_y () Real)
(declare-fun title_top_hight () Real)
(declare-fun back_ground_y () Real)
(declare-fun BC_y () Real)
(declare-fun back_ground_hight () Real)
(declare-fun BC_x () Real)
(declare-fun BC_width () Real)
(declare-fun BC_feasible () Bool)
(declare-fun BC_hight () Real)
(assert
 (let (($x2241 (not welcome_kid_3_feasible)))
 (let (($x3164 (or $x2241 welcome_kid_3_kid_4_feasible)))
 (let (($x3162 (not welcome_kid_3_kid_4_feasible)))
 (let (($x3163 (or $x3162 welcome_kid_3_feasible)))
 (let (($x3161 (or $x2241 welcome_kid_3_kid_3_feasible)))
 (let (($x3159 (not welcome_kid_3_kid_3_feasible)))
 (let (($x3160 (or $x3159 welcome_kid_3_feasible)))
 (let (($x3158 (or $x2241 welcome_kid_3_kid_2_feasible)))
 (let (($x3156 (not welcome_kid_3_kid_2_feasible)))
 (let (($x3157 (or $x3156 welcome_kid_3_feasible)))
 (let (($x3155 (or $x2241 welcome_kid_3_kid_1_feasible)))
 (let (($x3153 (not welcome_kid_3_kid_1_feasible)))
 (let (($x3154 (or $x3153 welcome_kid_3_feasible)))
 (let (($x3152 (or $x2241 welcome_kid_3_kid_0_feasible)))
 (let (($x3150 (not welcome_kid_3_kid_0_feasible)))
 (let (($x3151 (or $x3150 welcome_kid_3_feasible)))
 (let (($x2001 (not welcome_kid_2_feasible)))
 (let (($x3149 (or $x2001 welcome_kid_2_kid_5_feasible)))
 (let (($x3147 (not welcome_kid_2_kid_5_feasible)))
 (let (($x3148 (or $x3147 welcome_kid_2_feasible)))
 (let (($x3146 (or $x2001 welcome_kid_2_kid_4_feasible)))
 (let (($x3144 (not welcome_kid_2_kid_4_feasible)))
 (let (($x3145 (or $x3144 welcome_kid_2_feasible)))
 (let (($x3143 (or $x2001 welcome_kid_2_kid_3_feasible)))
 (let (($x3141 (not welcome_kid_2_kid_3_feasible)))
 (let (($x3142 (or $x3141 welcome_kid_2_feasible)))
 (let (($x3140 (or $x2001 welcome_kid_2_kid_2_feasible)))
 (let (($x3138 (not welcome_kid_2_kid_2_feasible)))
 (let (($x3139 (or $x3138 welcome_kid_2_feasible)))
 (let (($x3137 (or $x2001 welcome_kid_2_kid_1_feasible)))
 (let (($x3135 (not welcome_kid_2_kid_1_feasible)))
 (let (($x3136 (or $x3135 welcome_kid_2_feasible)))
 (let (($x3134 (or $x2001 welcome_kid_2_kid_0_feasible)))
 (let (($x3132 (not welcome_kid_2_kid_0_feasible)))
 (let (($x3133 (or $x3132 welcome_kid_2_feasible)))
 (let (($x1760 (not welcome_kid_1_feasible)))
 (let (($x3131 (or $x1760 welcome_kid_1_kid_5_feasible)))
 (let (($x3129 (not welcome_kid_1_kid_5_feasible)))
 (let (($x3130 (or $x3129 welcome_kid_1_feasible)))
 (let (($x3128 (or $x1760 welcome_kid_1_kid_4_feasible)))
 (let (($x3126 (not welcome_kid_1_kid_4_feasible)))
 (let (($x3127 (or $x3126 welcome_kid_1_feasible)))
 (let (($x3125 (or $x1760 welcome_kid_1_kid_3_feasible)))
 (let (($x3123 (not welcome_kid_1_kid_3_feasible)))
 (let (($x3124 (or $x3123 welcome_kid_1_feasible)))
 (let (($x3122 (or $x1760 welcome_kid_1_kid_2_feasible)))
 (let (($x3120 (not welcome_kid_1_kid_2_feasible)))
 (let (($x3121 (or $x3120 welcome_kid_1_feasible)))
 (let (($x3119 (or $x1760 welcome_kid_1_kid_1_feasible)))
 (let (($x3117 (not welcome_kid_1_kid_1_feasible)))
 (let (($x3118 (or $x3117 welcome_kid_1_feasible)))
 (let (($x3116 (or $x1760 welcome_kid_1_kid_0_feasible)))
 (let (($x3114 (not welcome_kid_1_kid_0_feasible)))
 (let (($x3115 (or $x3114 welcome_kid_1_feasible)))
 (let (($x1639 (not welcome_kid_0_feasible)))
 (let (($x3113 (or $x1639 welcome_kid_0_kid_2_feasible)))
 (let (($x3111 (not welcome_kid_0_kid_2_feasible)))
 (let (($x3112 (or $x3111 welcome_kid_0_feasible)))
 (let (($x3110 (or $x1639 welcome_kid_0_kid_1_feasible)))
 (let (($x3108 (not welcome_kid_0_kid_1_feasible)))
 (let (($x3109 (or $x3108 welcome_kid_0_feasible)))
 (let (($x3107 (or $x1639 welcome_kid_0_kid_0_feasible)))
 (let (($x3105 (not welcome_kid_0_kid_0_feasible)))
 (let (($x3106 (or $x3105 welcome_kid_0_feasible)))
 (let (($x1489 (not welcome_feasible)))
 (let (($x3104 (or $x1489 welcome_kid_3_feasible)))
 (let (($x3103 (or $x2241 welcome_feasible)))
 (let (($x3102 (or $x1489 welcome_kid_2_feasible)))
 (let (($x3101 (or $x2001 welcome_feasible)))
 (let (($x3100 (or $x1489 welcome_kid_1_feasible)))
 (let (($x3099 (or $x1760 welcome_feasible)))
 (let (($x3098 (or $x1489 welcome_kid_0_feasible)))
 (let (($x3097 (or $x1639 welcome_feasible)))
 (let (($x1345 (not ads2_feasible)))
 (let (($x1329 (not ads_feasible)))
 (let (($x3096 (or $x1329 $x1345 $x1489)))
 (let (($x3095 (or ads_feasible ads2_feasible $x1489)))
 (let (($x3094 (or $x1345 welcome_feasible)))
 (let (($x3093 (or $x1329 welcome_feasible)))
 (let (($x3090 (not pic_feasible)))
 (let (($x3092 (or $x1329 $x1345 $x3090)))
 (let (($x3091 (or ads_feasible ads2_feasible $x3090)))
 (let (($x3089 (or $x1345 pic_feasible)))
 (let (($x3088 (or $x1329 pic_feasible)))
 (let (($x3087 (or $x1329 side_bar_feasible)))
 (let (($x3085 (not side_bar_feasible)))
 (let (($x3086 (or $x3085 ads_feasible)))
 (let (($x3084 (= (- (* 5.0 rec_tbl_kid_24_width) (* 4.0 rec_tbl_kid_24_hight)) 0.0)))
 (let (($x3080 (= (- (* 5.0 rec_tbl_kid_23_width) (* 4.0 rec_tbl_kid_23_hight)) 0.0)))
 (let (($x3076 (= (+ (* (- 4.0) rec_tbl_kid_22_hight) (* 5.0 rec_tbl_kid_22_width)) 0.0)))
 (let (($x3072 (= (+ (* (- 4.0) rec_tbl_kid_21_hight) (* 5.0 rec_tbl_kid_21_width)) 0.0)))
 (let (($x3068 (= (+ (* (- 4.0) rec_tbl_kid_20_hight) (* 5.0 rec_tbl_kid_20_width)) 0.0)))
 (let (($x3064 (= (+ (* (- 4.0) rec_tbl_kid_19_hight) (* 5.0 rec_tbl_kid_19_width)) 0.0)))
 (let (($x3060 (= (+ (* (- 4.0) rec_tbl_kid_18_hight) (* 5.0 rec_tbl_kid_18_width)) 0.0)))
 (let (($x3056 (= (- (* 5.0 rec_tbl_kid_17_width) (* 4.0 rec_tbl_kid_17_hight)) 0.0)))
 (let (($x3052 (= (+ (* (- 4.0) rec_tbl_kid_16_hight) (* 5.0 rec_tbl_kid_16_width)) 0.0)))
 (let (($x3048 (= (+ (* (- 4.0) rec_tbl_kid_15_hight) (* 5.0 rec_tbl_kid_15_width)) 0.0)))
 (let (($x3044 (= (+ (* (- 4.0) rec_tbl_kid_14_hight) (* 5.0 rec_tbl_kid_14_width)) 0.0)))
 (let (($x3040 (= (+ (* (- 4.0) rec_tbl_kid_13_hight) (* 5.0 rec_tbl_kid_13_width)) 0.0)))
 (let (($x3036 (= (+ (* (- 4.0) rec_tbl_kid_12_hight) (* 5.0 rec_tbl_kid_12_width)) 0.0)))
 (let (($x3032 (= (- (* 5.0 rec_tbl_kid_11_width) (* 4.0 rec_tbl_kid_11_hight)) 0.0)))
 (let (($x3028 (= (- (* 5.0 rec_tbl_kid_10_width) (* 4.0 rec_tbl_kid_10_hight)) 0.0)))
 (let (($x3024 (= (+ (* (- 4.0) rec_tbl_kid_9_hight) (* 5.0 rec_tbl_kid_9_width)) 0.0)))
 (let (($x3020 (= (+ (* (- 4.0) rec_tbl_kid_8_hight) (* 5.0 rec_tbl_kid_8_width)) 0.0)))
 (let (($x3016 (= (+ (* (- 4.0) rec_tbl_kid_7_hight) (* 5.0 rec_tbl_kid_7_width)) 0.0)))
 (let (($x3012 (= (+ (* (- 4.0) rec_tbl_kid_6_hight) (* 5.0 rec_tbl_kid_6_width)) 0.0)))
 (let (($x3008 (= (- (* 5.0 rec_tbl_kid_5_width) (* 4.0 rec_tbl_kid_5_hight)) 0.0)))
 (let (($x3004 (= (- (* 5.0 rec_tbl_kid_4_width) (* 4.0 rec_tbl_kid_4_hight)) 0.0)))
 (let (($x3000 (= (- (* 5.0 rec_tbl_kid_3_width) (* 4.0 rec_tbl_kid_3_hight)) 0.0)))
 (let (($x2995 (= (+ (* (- 4.0) rec_tbl_kid_2_hight) (* 5.0 rec_tbl_kid_2_width)) 0.0)))
 (let (($x2991 (= (+ (* (- 4.0) rec_tbl_kid_1_hight) (* 5.0 rec_tbl_kid_1_width)) 0.0)))
 (let (($x2987 (= (+ (* (- 4.0) rec_tbl_kid_0_hight) (* 5.0 rec_tbl_kid_0_width)) 0.0)))
 (let (($x2981 (= (+ (- rec_tbl_kid_4_width) rec_tbl_kid_0_width) 0.0)))
 (let (($x2978 (= (+ (- rec_tbl_kid_3_width) rec_tbl_kid_0_width) 0.0)))
 (let (($x2975 (= (+ (- rec_tbl_kid_2_width) rec_tbl_kid_0_width) 0.0)))
 (let (($x2972 (= (- rec_tbl_kid_0_width rec_tbl_kid_1_width) 0.0)))
 (let (($x2970 (= (- rec_tbl_kid_0_hight rec_tbl_kid_20_hight) 0.0)))
 (let (($x2968 (= (- rec_tbl_kid_0_hight rec_tbl_kid_15_hight) 0.0)))
 (let (($x2966 (= (- rec_tbl_kid_0_hight rec_tbl_kid_10_hight) 0.0)))
 (let (($x2964 (= (- rec_tbl_kid_0_hight rec_tbl_kid_5_hight) 0.0)))
 (let ((?x2961 (- (+ (- (- 10.0) rec_tbl_kid_15_y) rec_tbl_kid_20_y) rec_tbl_kid_15_hight)))
 (let (($x2962 (= ?x2961 0.0)))
 (let ((?x2957 (- (- (+ (- 10.0) rec_tbl_kid_15_y) rec_tbl_kid_10_y) rec_tbl_kid_10_hight)))
 (let (($x2958 (= ?x2957 0.0)))
 (let ((?x2953 (- (+ (- (- 10.0) rec_tbl_kid_5_y) rec_tbl_kid_10_y) rec_tbl_kid_5_hight)))
 (let (($x2954 (= ?x2953 0.0)))
 (let ((?x2949 (- (+ (- (- 10.0) rec_tbl_kid_0_hight) rec_tbl_kid_5_y) rec_tbl_kid_0_y)))
 (let (($x2950 (= ?x2949 0.0)))
 (let ((?x2945 (+ (- (- (- 10.0) rec_tbl_kid_3_x) rec_tbl_kid_3_width) rec_tbl_kid_4_x)))
 (let (($x2946 (= ?x2945 0.0)))
 (let ((?x2941 (- (- (+ (- 10.0) rec_tbl_kid_3_x) rec_tbl_kid_2_x) rec_tbl_kid_2_width)))
 (let (($x2942 (= ?x2941 0.0)))
 (let ((?x2937 (- (- (+ (- 10.0) rec_tbl_kid_2_x) rec_tbl_kid_1_x) rec_tbl_kid_1_width)))
 (let (($x2938 (= ?x2937 0.0)))
 (let ((?x2933 (- (+ (- (- 10.0) rec_tbl_kid_0_x) rec_tbl_kid_1_x) rec_tbl_kid_0_width)))
 (let (($x2934 (= ?x2933 0.0)))
 (let (($x2930 (= (+ (- rec_tbl_kid_24_width) rec_tbl_kid_4_width) 0.0)))
 (let (($x2927 (= (- rec_tbl_kid_4_x rec_tbl_kid_24_x) 0.0)))
 (let (($x2925 (= (- rec_tbl_kid_4_width rec_tbl_kid_19_width) 0.0)))
 (let (($x2923 (= (+ (- rec_tbl_kid_19_x) rec_tbl_kid_4_x) 0.0)))
 (let (($x2920 (= (- rec_tbl_kid_4_width rec_tbl_kid_14_width) 0.0)))
 (let (($x2918 (= (+ (- rec_tbl_kid_14_x) rec_tbl_kid_4_x) 0.0)))
 (let (($x2915 (= (- rec_tbl_kid_4_width rec_tbl_kid_9_width) 0.0)))
 (let (($x2913 (= (+ (- rec_tbl_kid_9_x) rec_tbl_kid_4_x) 0.0)))
 (let (($x2910 (= (- rec_tbl_kid_3_width rec_tbl_kid_23_width) 0.0)))
 (let (($x2908 (= (- rec_tbl_kid_3_x rec_tbl_kid_23_x) 0.0)))
 (let (($x2906 (= (- rec_tbl_kid_3_width rec_tbl_kid_18_width) 0.0)))
 (let (($x2904 (= (- rec_tbl_kid_3_x rec_tbl_kid_18_x) 0.0)))
 (let (($x2902 (= (- rec_tbl_kid_3_width rec_tbl_kid_13_width) 0.0)))
 (let (($x2900 (= (- rec_tbl_kid_3_x rec_tbl_kid_13_x) 0.0)))
 (let (($x2898 (= (- rec_tbl_kid_3_width rec_tbl_kid_8_width) 0.0)))
 (let (($x2896 (= (- rec_tbl_kid_3_x rec_tbl_kid_8_x) 0.0)))
 (let (($x2894 (= (- rec_tbl_kid_2_width rec_tbl_kid_22_width) 0.0)))
 (let (($x2892 (= (+ (- rec_tbl_kid_22_x) rec_tbl_kid_2_x) 0.0)))
 (let (($x2889 (= (+ (- rec_tbl_kid_17_width) rec_tbl_kid_2_width) 0.0)))
 (let (($x2886 (= (- rec_tbl_kid_2_x rec_tbl_kid_17_x) 0.0)))
 (let (($x2884 (= (- rec_tbl_kid_2_width rec_tbl_kid_12_width) 0.0)))
 (let (($x2882 (= (- rec_tbl_kid_2_x rec_tbl_kid_12_x) 0.0)))
 (let (($x2880 (= (- rec_tbl_kid_2_width rec_tbl_kid_7_width) 0.0)))
 (let (($x2878 (= (- rec_tbl_kid_2_x rec_tbl_kid_7_x) 0.0)))
 (let (($x2876 (= (+ (- rec_tbl_kid_21_width) rec_tbl_kid_1_width) 0.0)))
 (let (($x2873 (= (+ (- rec_tbl_kid_21_x) rec_tbl_kid_1_x) 0.0)))
 (let (($x2870 (= (+ (- rec_tbl_kid_16_width) rec_tbl_kid_1_width) 0.0)))
 (let (($x2867 (= (+ (- rec_tbl_kid_16_x) rec_tbl_kid_1_x) 0.0)))
 (let (($x2864 (= (+ (- rec_tbl_kid_11_width) rec_tbl_kid_1_width) 0.0)))
 (let (($x2861 (= (- rec_tbl_kid_1_x rec_tbl_kid_11_x) 0.0)))
 (let (($x2859 (= (- rec_tbl_kid_1_width rec_tbl_kid_6_width) 0.0)))
 (let (($x2857 (= (- rec_tbl_kid_1_x rec_tbl_kid_6_x) 0.0)))
 (let (($x2855 (= (- rec_tbl_kid_0_width rec_tbl_kid_20_width) 0.0)))
 (let (($x2853 (= (- rec_tbl_kid_0_x rec_tbl_kid_20_x) 0.0)))
 (let (($x2851 (= (- rec_tbl_kid_0_width rec_tbl_kid_15_width) 0.0)))
 (let (($x2849 (= (- rec_tbl_kid_0_x rec_tbl_kid_15_x) 0.0)))
 (let (($x2847 (= (+ (- rec_tbl_kid_10_width) rec_tbl_kid_0_width) 0.0)))
 (let (($x2844 (= (- rec_tbl_kid_0_x rec_tbl_kid_10_x) 0.0)))
 (let (($x2842 (= (+ (- rec_tbl_kid_5_width) rec_tbl_kid_0_width) 0.0)))
 (let (($x2839 (= (- rec_tbl_kid_0_x rec_tbl_kid_5_x) 0.0)))
 (let (($x2837 (= (- rec_tbl_kid_20_hight rec_tbl_kid_24_hight) 0.0)))
 (let (($x2835 (= (- rec_tbl_kid_20_y rec_tbl_kid_24_y) 0.0)))
 (let (($x2833 (= (- rec_tbl_kid_20_hight rec_tbl_kid_23_hight) 0.0)))
 (let (($x2831 (= (- rec_tbl_kid_20_y rec_tbl_kid_23_y) 0.0)))
 (let (($x2829 (= (+ (- rec_tbl_kid_22_hight) rec_tbl_kid_20_hight) 0.0)))
 (let (($x2826 (= (- rec_tbl_kid_20_y rec_tbl_kid_22_y) 0.0)))
 (let (($x2824 (= (+ (- rec_tbl_kid_21_hight) rec_tbl_kid_20_hight) 0.0)))
 (let (($x2821 (= (- rec_tbl_kid_20_y rec_tbl_kid_21_y) 0.0)))
 (let (($x2819 (= (- rec_tbl_kid_15_hight rec_tbl_kid_19_hight) 0.0)))
 (let (($x2817 (= (- rec_tbl_kid_15_y rec_tbl_kid_19_y) 0.0)))
 (let (($x2815 (= (- rec_tbl_kid_15_hight rec_tbl_kid_18_hight) 0.0)))
 (let (($x2813 (= (- rec_tbl_kid_15_y rec_tbl_kid_18_y) 0.0)))
 (let (($x2811 (= (- rec_tbl_kid_15_hight rec_tbl_kid_17_hight) 0.0)))
 (let (($x2809 (= (- rec_tbl_kid_15_y rec_tbl_kid_17_y) 0.0)))
 (let (($x2807 (= (+ (- rec_tbl_kid_16_hight) rec_tbl_kid_15_hight) 0.0)))
 (let (($x2804 (= (- rec_tbl_kid_15_y rec_tbl_kid_16_y) 0.0)))
 (let (($x2802 (= (+ (- rec_tbl_kid_14_hight) rec_tbl_kid_10_hight) 0.0)))
 (let (($x2799 (= (- rec_tbl_kid_10_y rec_tbl_kid_14_y) 0.0)))
 (let (($x2797 (= (+ (- rec_tbl_kid_13_hight) rec_tbl_kid_10_hight) 0.0)))
 (let (($x2794 (= (+ (- rec_tbl_kid_13_y) rec_tbl_kid_10_y) 0.0)))
 (let (($x2791 (= (+ (- rec_tbl_kid_12_hight) rec_tbl_kid_10_hight) 0.0)))
 (let (($x2788 (= (+ (- rec_tbl_kid_12_y) rec_tbl_kid_10_y) 0.0)))
 (let (($x2785 (= (- rec_tbl_kid_10_hight rec_tbl_kid_11_hight) 0.0)))
 (let (($x2783 (= (+ (- rec_tbl_kid_11_y) rec_tbl_kid_10_y) 0.0)))
 (let (($x2780 (= (+ (- rec_tbl_kid_9_hight) rec_tbl_kid_5_hight) 0.0)))
 (let (($x2777 (= (- rec_tbl_kid_5_y rec_tbl_kid_9_y) 0.0)))
 (let (($x2775 (= (+ (- rec_tbl_kid_8_hight) rec_tbl_kid_5_hight) 0.0)))
 (let (($x2772 (= (- rec_tbl_kid_5_y rec_tbl_kid_8_y) 0.0)))
 (let (($x2770 (= (+ (- rec_tbl_kid_7_hight) rec_tbl_kid_5_hight) 0.0)))
 (let (($x2767 (= (- rec_tbl_kid_5_y rec_tbl_kid_7_y) 0.0)))
 (let (($x2765 (= (+ (- rec_tbl_kid_6_hight) rec_tbl_kid_5_hight) 0.0)))
 (let (($x2762 (= (+ (- rec_tbl_kid_6_y) rec_tbl_kid_5_y) 0.0)))
 (let (($x2759 (= (- rec_tbl_kid_0_hight rec_tbl_kid_4_hight) 0.0)))
 (let (($x2757 (= (+ (- rec_tbl_kid_4_y) rec_tbl_kid_0_y) 0.0)))
 (let (($x2754 (= (- rec_tbl_kid_0_hight rec_tbl_kid_3_hight) 0.0)))
 (let (($x2752 (= (+ (- rec_tbl_kid_3_y) rec_tbl_kid_0_y) 0.0)))
 (let (($x2749 (= (+ (- rec_tbl_kid_2_hight) rec_tbl_kid_0_hight) 0.0)))
 (let (($x2746 (= (+ (- rec_tbl_kid_2_y) rec_tbl_kid_0_y) 0.0)))
 (let (($x2743 (= (- rec_tbl_kid_0_hight rec_tbl_kid_1_hight) 0.0)))
 (let (($x2741 (= (+ (- rec_tbl_kid_1_y) rec_tbl_kid_0_y) 0.0)))
 (let ((?x2737 (+ (- (+ (- rec_tbl_y) rec_tbl_kid_24_y) rec_tbl_hight) rec_tbl_kid_24_hight)))
 (let (($x2738 (= ?x2737 (- 10.0))))
 (let ((?x2733 (+ (- (- rec_tbl_kid_24_width rec_tbl_x) rec_tbl_width) rec_tbl_kid_24_x)))
 (let (($x2734 (= ?x2733 (- 10.0))))
 (let (($x2730 (= (+ (- rec_tbl_y) rec_tbl_kid_0_y) 10.0)))
 (let (($x2728 (= (- rec_tbl_kid_0_x rec_tbl_x) 10.0)))
 (let ((?x2725 (+ (- (+ (- recommend_x) rec_tbl_x) recommend_width) rec_tbl_width)))
 (let (($x2726 (= ?x2725 0.0)))
 (let ((?x1280 (- recommend_x)))
 (let ((?x2426 (+ ?x1280 rec_tbl_x)))
 (let (($x2723 (= ?x2426 0.0)))
 (let (($x2722 (>= rec_tbl_kid_24_hight 0.0)))
 (let (($x2721 (>= rec_tbl_kid_24_width 0.0)))
 (let (($x2720 (>= rec_tbl_kid_24_y 0.0)))
 (let (($x2719 (>= rec_tbl_kid_24_x 0.0)))
 (let (($x2718 (>= rec_tbl_kid_23_hight 0.0)))
 (let (($x2717 (>= rec_tbl_kid_23_width 0.0)))
 (let (($x2716 (>= rec_tbl_kid_23_y 0.0)))
 (let (($x2715 (>= rec_tbl_kid_23_x 0.0)))
 (let (($x2714 (>= rec_tbl_kid_22_hight 0.0)))
 (let (($x2713 (>= rec_tbl_kid_22_width 0.0)))
 (let (($x2712 (>= rec_tbl_kid_22_y 0.0)))
 (let (($x2711 (>= rec_tbl_kid_22_x 0.0)))
 (let (($x2710 (>= rec_tbl_kid_21_hight 0.0)))
 (let (($x2709 (>= rec_tbl_kid_21_width 0.0)))
 (let (($x2708 (>= rec_tbl_kid_21_y 0.0)))
 (let (($x2707 (>= rec_tbl_kid_21_x 0.0)))
 (let (($x2706 (>= rec_tbl_kid_20_hight 0.0)))
 (let (($x2705 (>= rec_tbl_kid_20_width 0.0)))
 (let (($x2704 (>= rec_tbl_kid_20_y 0.0)))
 (let (($x2703 (>= rec_tbl_kid_20_x 0.0)))
 (let (($x2702 (>= rec_tbl_kid_19_hight 0.0)))
 (let (($x2701 (>= rec_tbl_kid_19_width 0.0)))
 (let (($x2700 (>= rec_tbl_kid_19_y 0.0)))
 (let (($x2699 (>= rec_tbl_kid_19_x 0.0)))
 (let (($x2698 (>= rec_tbl_kid_18_hight 0.0)))
 (let (($x2697 (>= rec_tbl_kid_18_width 0.0)))
 (let (($x2696 (>= rec_tbl_kid_18_y 0.0)))
 (let (($x2695 (>= rec_tbl_kid_18_x 0.0)))
 (let (($x2694 (>= rec_tbl_kid_17_hight 0.0)))
 (let (($x2693 (>= rec_tbl_kid_17_width 0.0)))
 (let (($x2692 (>= rec_tbl_kid_17_y 0.0)))
 (let (($x2691 (>= rec_tbl_kid_17_x 0.0)))
 (let (($x2690 (>= rec_tbl_kid_16_hight 0.0)))
 (let (($x2689 (>= rec_tbl_kid_16_width 0.0)))
 (let (($x2688 (>= rec_tbl_kid_16_y 0.0)))
 (let (($x2687 (>= rec_tbl_kid_16_x 0.0)))
 (let (($x2686 (>= rec_tbl_kid_15_hight 0.0)))
 (let (($x2685 (>= rec_tbl_kid_15_width 0.0)))
 (let (($x2684 (>= rec_tbl_kid_15_y 0.0)))
 (let (($x2683 (>= rec_tbl_kid_15_x 0.0)))
 (let (($x2682 (>= rec_tbl_kid_14_hight 0.0)))
 (let (($x2681 (>= rec_tbl_kid_14_width 0.0)))
 (let (($x2680 (>= rec_tbl_kid_14_y 0.0)))
 (let (($x2679 (>= rec_tbl_kid_14_x 0.0)))
 (let (($x2678 (>= rec_tbl_kid_13_hight 0.0)))
 (let (($x2677 (>= rec_tbl_kid_13_width 0.0)))
 (let (($x2676 (>= rec_tbl_kid_13_y 0.0)))
 (let (($x2675 (>= rec_tbl_kid_13_x 0.0)))
 (let (($x2674 (>= rec_tbl_kid_12_hight 0.0)))
 (let (($x2673 (>= rec_tbl_kid_12_width 0.0)))
 (let (($x2672 (>= rec_tbl_kid_12_y 0.0)))
 (let (($x2671 (>= rec_tbl_kid_12_x 0.0)))
 (let (($x2670 (>= rec_tbl_kid_11_hight 0.0)))
 (let (($x2669 (>= rec_tbl_kid_11_width 0.0)))
 (let (($x2668 (>= rec_tbl_kid_11_y 0.0)))
 (let (($x2667 (>= rec_tbl_kid_11_x 0.0)))
 (let (($x2666 (>= rec_tbl_kid_10_hight 0.0)))
 (let (($x2665 (>= rec_tbl_kid_10_width 0.0)))
 (let (($x2664 (>= rec_tbl_kid_10_y 0.0)))
 (let (($x2663 (>= rec_tbl_kid_10_x 0.0)))
 (let (($x2662 (>= rec_tbl_kid_9_hight 0.0)))
 (let (($x2661 (>= rec_tbl_kid_9_width 0.0)))
 (let (($x2660 (>= rec_tbl_kid_9_y 0.0)))
 (let (($x2659 (>= rec_tbl_kid_9_x 0.0)))
 (let (($x2658 (>= rec_tbl_kid_8_hight 0.0)))
 (let (($x2657 (>= rec_tbl_kid_8_width 0.0)))
 (let (($x2656 (>= rec_tbl_kid_8_y 0.0)))
 (let (($x2655 (>= rec_tbl_kid_8_x 0.0)))
 (let (($x2654 (>= rec_tbl_kid_7_hight 0.0)))
 (let (($x2653 (>= rec_tbl_kid_7_width 0.0)))
 (let (($x2652 (>= rec_tbl_kid_7_y 0.0)))
 (let (($x2651 (>= rec_tbl_kid_7_x 0.0)))
 (let (($x2650 (>= rec_tbl_kid_6_hight 0.0)))
 (let (($x2649 (>= rec_tbl_kid_6_width 0.0)))
 (let (($x2648 (>= rec_tbl_kid_6_y 0.0)))
 (let (($x2647 (>= rec_tbl_kid_6_x 0.0)))
 (let (($x2646 (>= rec_tbl_kid_5_hight 0.0)))
 (let (($x2645 (>= rec_tbl_kid_5_width 0.0)))
 (let (($x2644 (>= rec_tbl_kid_5_y 0.0)))
 (let (($x2643 (>= rec_tbl_kid_5_x 0.0)))
 (let (($x2642 (>= rec_tbl_kid_4_hight 0.0)))
 (let (($x2641 (>= rec_tbl_kid_4_width 0.0)))
 (let (($x2640 (>= rec_tbl_kid_4_y 0.0)))
 (let (($x2639 (>= rec_tbl_kid_4_x 0.0)))
 (let (($x2638 (>= rec_tbl_kid_3_hight 0.0)))
 (let (($x2637 (>= rec_tbl_kid_3_width 0.0)))
 (let (($x2636 (>= rec_tbl_kid_3_y 0.0)))
 (let (($x2635 (>= rec_tbl_kid_3_x 0.0)))
 (let (($x2634 (>= rec_tbl_kid_2_hight 0.0)))
 (let (($x2633 (>= rec_tbl_kid_2_width 0.0)))
 (let (($x2632 (>= rec_tbl_kid_2_y 0.0)))
 (let (($x2631 (>= rec_tbl_kid_2_x 0.0)))
 (let (($x2630 (>= rec_tbl_kid_1_hight 0.0)))
 (let (($x2629 (>= rec_tbl_kid_1_width 0.0)))
 (let (($x2628 (>= rec_tbl_kid_1_y 0.0)))
 (let (($x2627 (>= rec_tbl_kid_1_x 0.0)))
 (let (($x2626 (>= rec_tbl_kid_0_hight 0.0)))
 (let (($x2625 (>= rec_tbl_kid_0_width 0.0)))
 (let (($x2624 (>= rec_tbl_kid_0_y 0.0)))
 (let (($x2623 (>= rec_tbl_kid_0_x 0.0)))
 (let ((?x2599 (- (+ (- select_kid_4_width) select_kid_5_x) select_kid_4_x)))
 (let (($x2622 (= ?x2599 0.0)))
 (let ((?x2596 (+ (- (- select_kid_3_width) select_kid_3_x) select_kid_4_x)))
 (let (($x2621 (= ?x2596 0.0)))
 (let ((?x2593 (- (+ (- select_kid_2_width) select_kid_3_x) select_kid_2_x)))
 (let (($x2620 (= ?x2593 0.0)))
 (let ((?x2529 (- (- select_kid_1_x) select_kid_1_width)))
 (let ((?x2590 (+ ?x2529 select_kid_2_x)))
 (let (($x2619 (= ?x2590 0.0)))
 (let ((?x2588 (- (- select_kid_1_x select_kid_0_x) select_kid_0_width)))
 (let (($x2618 (= ?x2588 0.0)))
 (let (($x2617 (= (- select_kid_0_width select_kid_5_width) 0.0)))
 (let (($x2615 (= (+ (- select_kid_4_width) select_kid_0_width) 0.0)))
 (let (($x2613 (= (+ (- select_kid_3_width) select_kid_0_width) 0.0)))
 (let (($x2611 (= (+ (- select_kid_2_width) select_kid_0_width) 0.0)))
 (let (($x2609 (= (+ (- select_kid_1_width) select_kid_0_width) 0.0)))
 (let (($x2606 (= select_hight 50.0)))
 (let (($x2605 (= (+ (+ (- ?x1280 recommend_width) select_x) select_width) 0.0)))
 (let ((?x2413 (+ ?x1280 select_x)))
 (let (($x2601 (= ?x2413 0.0)))
 (let (($x2600 (>= ?x2599 0.0)))
 (let (($x2597 (>= ?x2596 0.0)))
 (let (($x2594 (>= ?x2593 0.0)))
 (let (($x2591 (>= ?x2590 0.0)))
 (let (($x2589 (>= ?x2588 0.0)))
 (let ((?x2585 (+ (- (+ (- select_kid_5_y) select_y) select_kid_5_hight) select_hight)))
 (let (($x2586 (>= ?x2585 0.0)))
 (let ((?x2492 (- select_kid_5_y select_y)))
 (let (($x2581 (>= ?x2492 0.0)))
 (let ((?x2579 (+ (- (+ (- select_kid_5_x) select_x) select_kid_5_width) select_width)))
 (let (($x2580 (>= ?x2579 0.0)))
 (let ((?x2478 (- select_kid_5_x select_x)))
 (let (($x2575 (>= ?x2478 0.0)))
 (let ((?x2573 (- (+ (- select_y select_kid_4_y) select_hight) select_kid_4_hight)))
 (let (($x2574 (>= ?x2573 0.0)))
 (let ((?x2421 (- select_y)))
 (let ((?x2490 (+ ?x2421 select_kid_4_y)))
 (let (($x2570 (>= ?x2490 0.0)))
 (let ((?x2568 (+ (- (+ (- select_kid_4_width) select_x) select_kid_4_x) select_width)))
 (let (($x2569 (>= ?x2568 0.0)))
 (let (($x2564 (>= (+ (- select_x) select_kid_4_x) 0.0)))
 (let ((?x2561 (- (- (+ select_y select_hight) select_kid_3_y) select_kid_3_hight)))
 (let (($x2562 (>= ?x2561 0.0)))
 (let ((?x2488 (+ ?x2421 select_kid_3_y)))
 (let (($x2559 (>= ?x2488 0.0)))
 (let ((?x2557 (+ (- (+ (- select_kid_3_width) select_x) select_kid_3_x) select_width)))
 (let (($x2558 (>= ?x2557 0.0)))
 (let (($x2553 (>= (+ (- select_x) select_kid_3_x) 0.0)))
 (let ((?x2550 (- (- (+ select_y select_hight) select_kid_2_y) select_kid_2_hight)))
 (let (($x2551 (>= ?x2550 0.0)))
 (let ((?x2486 (+ ?x2421 select_kid_2_y)))
 (let (($x2547 (>= ?x2486 0.0)))
 (let ((?x2545 (- (+ (+ (- select_kid_2_width) select_x) select_width) select_kid_2_x)))
 (let (($x2546 (>= ?x2545 0.0)))
 (let (($x2541 (>= (+ (- select_x) select_kid_2_x) 0.0)))
 (let ((?x2537 (- (+ (+ (- select_kid_1_hight) select_y) select_hight) select_kid_1_y)))
 (let (($x2538 (>= ?x2537 0.0)))
 (let ((?x2484 (+ ?x2421 select_kid_1_y)))
 (let (($x2533 (>= ?x2484 0.0)))
 (let (($x2532 (>= (+ (+ ?x2529 select_x) select_width) 0.0)))
 (let (($x2527 (>= (- select_kid_1_x select_x) 0.0)))
 (let ((?x2524 (+ (- (+ (- select_kid_0_y) select_y) select_kid_0_hight) select_hight)))
 (let (($x2525 (>= ?x2524 0.0)))
 (let ((?x2482 (- select_kid_0_y select_y)))
 (let (($x2520 (>= ?x2482 0.0)))
 (let ((?x2518 (+ (- (+ (- select_kid_0_x) select_x) select_kid_0_width) select_width)))
 (let (($x2519 (>= ?x2518 0.0)))
 (let ((?x2476 (- select_kid_0_x select_x)))
 (let (($x2514 (>= ?x2476 0.0)))
 (let (($x2513 (= (- (+ ?x2492 select_kid_5_hight) select_hight) 0.0)))
 (let (($x2510 (= (+ (- ?x2490 select_hight) select_kid_4_hight) 0.0)))
 (let (($x2507 (= (+ (+ (- ?x2421 select_hight) select_kid_3_y) select_kid_3_hight) 0.0)))
 (let (($x2504 (= (+ (+ (- ?x2421 select_hight) select_kid_2_y) select_kid_2_hight) 0.0)))
 (let ((?x2499 (+ (- (- select_kid_1_hight select_y) select_hight) select_kid_1_y)))
 (let (($x2500 (= ?x2499 0.0)))
 (let (($x2496 (= (- (+ ?x2482 select_kid_0_hight) select_hight) 0.0)))
 (let (($x2493 (= ?x2492 0.0)))
 (let (($x2491 (= ?x2490 0.0)))
 (let (($x2489 (= ?x2488 0.0)))
 (let (($x2487 (= ?x2486 0.0)))
 (let (($x2485 (= ?x2484 0.0)))
 (let (($x2483 (= ?x2482 0.0)))
 (let (($x2481 (= (- (+ ?x2478 select_kid_5_width) select_width) 0.0)))
 (let (($x2477 (= ?x2476 0.0)))
 (let (($x2475 (>= select_kid_5_hight 0.0)))
 (let (($x2474 (>= select_kid_5_width 0.0)))
 (let (($x2473 (>= select_kid_5_y 0.0)))
 (let (($x2472 (>= select_kid_5_x 0.0)))
 (let (($x2471 (>= select_kid_4_hight 0.0)))
 (let (($x2470 (>= select_kid_4_width 0.0)))
 (let (($x2469 (>= select_kid_4_y 0.0)))
 (let (($x2468 (>= select_kid_4_x 0.0)))
 (let (($x2467 (>= select_kid_3_hight 0.0)))
 (let (($x2466 (>= select_kid_3_width 0.0)))
 (let (($x2465 (>= select_kid_3_y 0.0)))
 (let (($x2464 (>= select_kid_3_x 0.0)))
 (let (($x2463 (>= select_kid_2_hight 0.0)))
 (let (($x2462 (>= select_kid_2_width 0.0)))
 (let (($x2461 (>= select_kid_2_y 0.0)))
 (let (($x2460 (>= select_kid_2_x 0.0)))
 (let (($x2459 (>= select_kid_1_hight 0.0)))
 (let (($x2458 (>= select_kid_1_width 0.0)))
 (let (($x2457 (>= select_kid_1_y 0.0)))
 (let (($x2456 (>= select_kid_1_x 0.0)))
 (let (($x2455 (>= select_kid_0_hight 0.0)))
 (let (($x2454 (>= select_kid_0_width 0.0)))
 (let (($x2453 (>= select_kid_0_y 0.0)))
 (let (($x2452 (>= select_kid_0_x 0.0)))
 (let ((?x2407 (- rec_title_y recommend_y)))
 (let (($x2451 (= ?x2407 10.0)))
 (let ((?x2448 (* 2.0 rec_title_x)))
 (let ((?x2449 (+ (- (- rec_title_width (* 2.0 recommend_x)) recommend_width) ?x2448)))
 (let (($x2450 (= ?x2449 0.0)))
 (let (($x2444 (= (+ (- 50.0) rec_title_hight) 0.0)))
 (let (($x2442 (= (+ (- 100.0) rec_title_width) 0.0)))
 (let ((?x2398 (- (- rec_tbl_y select_y) select_hight)))
 (let (($x2440 (>= ?x2398 0.0)))
 (let ((?x2395 (- (- select_y rec_title_y) rec_title_hight)))
 (let (($x2439 (>= ?x2395 0.0)))
 (let ((?x2437 (+ (- (+ (- rec_tbl_y) recommend_hight) rec_tbl_hight) recommend_y)))
 (let (($x2438 (>= ?x2437 0.0)))
 (let (($x2433 (>= (- rec_tbl_y recommend_y) 0.0)))
 (let (($x2431 (>= (- (+ (- recommend_x rec_tbl_x) recommend_width) rec_tbl_width) 0.0)))
 (let (($x2427 (>= ?x2426 0.0)))
 (let (($x2425 (>= (+ (- (+ ?x2421 recommend_hight) select_hight) recommend_y) 0.0)))
 (let (($x2420 (>= (- select_y recommend_y) 0.0)))
 (let (($x2418 (>= (- (- (+ recommend_x recommend_width) select_x) select_width) 0.0)))
 (let (($x2414 (>= ?x2413 0.0)))
 (let ((?x2411 (+ (- (- recommend_hight rec_title_y) rec_title_hight) recommend_y)))
 (let (($x2412 (>= ?x2411 0.0)))
 (let (($x2408 (>= ?x2407 0.0)))
 (let ((?x2405 (- (+ (+ (- rec_title_width) recommend_x) recommend_width) rec_title_x)))
 (let (($x2406 (>= ?x2405 0.0)))
 (let (($x2401 (>= (+ ?x1280 rec_title_x) 0.0)))
 (let (($x2399 (= ?x2398 10.0)))
 (let (($x2396 (= ?x2395 10.0)))
 (let (($x2393 (>= rec_tbl_hight 0.0)))
 (let (($x2392 (>= rec_tbl_width 0.0)))
 (let (($x2391 (>= rec_tbl_y 0.0)))
 (let (($x2390 (>= rec_tbl_x 0.0)))
 (let (($x2389 (>= select_hight 0.0)))
 (let (($x2388 (>= select_width 0.0)))
 (let (($x2387 (>= select_y 0.0)))
 (let (($x2386 (>= select_x 0.0)))
 (let (($x2385 (>= rec_title_hight 0.0)))
 (let (($x2384 (>= rec_title_width 0.0)))
 (let (($x2383 (>= rec_title_y 0.0)))
 (let (($x2382 (>= rec_title_x 0.0)))
 (let (($x2380 (= (- (- (+ welcome_y welcome_hight) ads2_y) ads2_hight) 0.0)))
 (let (($x2381 (or $x1345 $x2380)))
 (let (($x2377 (or $x1345 (= (- welcome_y ads2_y) 0.0))))
 (let (($x2375 (or $x1345 (= (- (+ (- pic_y ads2_y) pic_hight) ads2_hight) 0.0))))
 (let (($x2371 (or $x1345 (= (- pic_y ads2_y) 0.0))))
 (let ((?x2366 (* 2.0 ads2_x)))
 (let ((?x2367 (- (+ (+ (+ (- ads2_width) pic_x) welcome_x) welcome_width) ?x2366)))
 (let (($x2369 (or $x1345 (= ?x2367 0.0))))
 (let (($x2361 (or $x1345 (= (+ (- (- (- 10.0) pic_width) pic_x) welcome_x) 0.0))))
 (let (($x2356 (or $x1345 (= pic_width 400.0))))
 (let ((?x1432 (+ (- (- pic_width) pic_x) welcome_x)))
 (let (($x1433 (>= ?x1432 0.0)))
 (let (($x2353 (or $x1345 $x1433)))
 (let (($x2351 (>= (+ (+ (- (- welcome_y) welcome_hight) ads2_y) ads2_hight) 0.0)))
 (let (($x2352 (or $x1345 $x2351)))
 (let (($x2348 (or $x1345 (>= (- welcome_y ads2_y) 0.0))))
 (let (($x2344 (>= (+ (- (- ads2_width welcome_x) welcome_width) ads2_x) 0.0)))
 (let (($x2345 (or $x1345 $x2344)))
 (let (($x2340 (or $x1345 (>= (- welcome_x ads2_x) 0.0))))
 (let (($x2337 (or $x1345 (>= (+ (- (+ (- pic_y) ads2_y) pic_hight) ads2_hight) 0.0))))
 (let (($x2331 (or $x1345 (>= (- pic_y ads2_y) 0.0))))
 (let (($x2328 (or $x1345 (>= (+ (- (+ (- pic_width) ads2_width) pic_x) ads2_x) 0.0))))
 (let (($x2323 (or $x1345 (>= (- pic_x ads2_x) 0.0))))
 (let (($x2320 (or $x2241 (= (+ (- welcome_kid_3_kid_4_width) welcome_kid_3_kid_0_width) 0.0))))
 (let (($x2316 (or $x2241 (= (+ (- welcome_kid_3_kid_3_width) welcome_kid_3_kid_0_width) 0.0))))
 (let (($x2312 (or $x2241 (= (+ (- welcome_kid_3_kid_2_width) welcome_kid_3_kid_0_width) 0.0))))
 (let (($x2308 (or $x2241 (= (- welcome_kid_3_kid_0_width welcome_kid_3_kid_1_width) 0.0))))
 (let ((?x2303 (+ (- (- (- 40.0) welcome_kid_3_kid_3_x) welcome_kid_3_kid_3_width) welcome_kid_3_kid_4_x)))
 (let (($x2305 (or $x2241 (= ?x2303 0.0))))
 (let ((?x2298 (- (- (+ (- 40.0) welcome_kid_3_kid_3_x) welcome_kid_3_kid_2_x) welcome_kid_3_kid_2_width)))
 (let (($x2300 (or $x2241 (= ?x2298 0.0))))
 (let ((?x2293 (- (- (+ (- 40.0) welcome_kid_3_kid_2_x) welcome_kid_3_kid_1_x) welcome_kid_3_kid_1_width)))
 (let (($x2295 (or $x2241 (= ?x2293 0.0))))
 (let ((?x2288 (- (+ (- (- 40.0) welcome_kid_3_kid_0_x) welcome_kid_3_kid_1_x) welcome_kid_3_kid_0_width)))
 (let (($x2290 (or $x2241 (= ?x2288 0.0))))
 (let (($x2284 (or $x2241 (= (- welcome_kid_3_kid_0_hight welcome_kid_3_kid_4_hight) 0.0))))
 (let (($x2281 (or $x2241 (= (- welcome_kid_3_kid_0_y welcome_kid_3_kid_4_y) 0.0))))
 (let (($x2278 (or $x2241 (= (- welcome_kid_3_kid_0_hight welcome_kid_3_kid_3_hight) 0.0))))
 (let (($x2275 (or $x2241 (= (- welcome_kid_3_kid_0_y welcome_kid_3_kid_3_y) 0.0))))
 (let (($x2272 (or $x2241 (= (+ (- welcome_kid_3_kid_2_hight) welcome_kid_3_kid_0_hight) 0.0))))
 (let (($x2268 (or $x2241 (= (- welcome_kid_3_kid_0_y welcome_kid_3_kid_2_y) 0.0))))
 (let (($x2265 (or $x2241 (= (+ (- welcome_kid_3_kid_1_hight) welcome_kid_3_kid_0_hight) 0.0))))
 (let (($x2261 (or $x2241 (= (- welcome_kid_3_kid_0_y welcome_kid_3_kid_1_y) 0.0))))
 (let ((?x2255 (- (+ (- welcome_kid_3_y) welcome_kid_3_kid_4_y) welcome_kid_3_hight)))
 (let (($x2258 (or $x2241 (= (+ ?x2255 welcome_kid_3_kid_4_hight) (- 10.0)))))
 (let ((?x2249 (+ (+ (- welcome_kid_3_width) welcome_kid_3_kid_4_width) welcome_kid_3_kid_4_x)))
 (let (($x2252 (or $x2241 (= (- ?x2249 welcome_kid_3_x) (- 10.0)))))
 (let (($x2247 (or $x2241 (= (- welcome_kid_3_kid_0_y welcome_kid_3_y) 10.0))))
 (let (($x2244 (or $x2241 (= (- welcome_kid_3_kid_0_x welcome_kid_3_x) 10.0))))
 (let (($x2240 (>= welcome_kid_3_kid_4_hight 0.0)))
 (let (($x2239 (>= welcome_kid_3_kid_4_width 0.0)))
 (let (($x2238 (>= welcome_kid_3_kid_4_y 0.0)))
 (let (($x2237 (>= welcome_kid_3_kid_4_x 0.0)))
 (let (($x2236 (>= welcome_kid_3_kid_3_hight 0.0)))
 (let (($x2235 (>= welcome_kid_3_kid_3_width 0.0)))
 (let (($x2234 (>= welcome_kid_3_kid_3_y 0.0)))
 (let (($x2233 (>= welcome_kid_3_kid_3_x 0.0)))
 (let (($x2232 (>= welcome_kid_3_kid_2_hight 0.0)))
 (let (($x2231 (>= welcome_kid_3_kid_2_width 0.0)))
 (let (($x2230 (>= welcome_kid_3_kid_2_y 0.0)))
 (let (($x2229 (>= welcome_kid_3_kid_2_x 0.0)))
 (let (($x2228 (>= welcome_kid_3_kid_1_hight 0.0)))
 (let (($x2227 (>= welcome_kid_3_kid_1_width 0.0)))
 (let (($x2226 (>= welcome_kid_3_kid_1_y 0.0)))
 (let (($x2225 (>= welcome_kid_3_kid_1_x 0.0)))
 (let (($x2224 (>= welcome_kid_3_kid_0_hight 0.0)))
 (let (($x2223 (>= welcome_kid_3_kid_0_width 0.0)))
 (let (($x2222 (>= welcome_kid_3_kid_0_y 0.0)))
 (let (($x2221 (>= welcome_kid_3_kid_0_x 0.0)))
 (let ((?x2215 (+ (- (- welcome_kid_2_kid_4_width) welcome_kid_2_kid_1_x) welcome_kid_2_kid_0_x)))
 (let ((?x2218 (- (+ (+ ?x2215 welcome_kid_2_kid_5_x) welcome_kid_2_kid_0_width) welcome_kid_2_kid_4_x)))
 (let (($x2220 (or $x2001 (= ?x2218 0.0))))
 (let ((?x2208 (- (- (- welcome_kid_2_kid_3_x) welcome_kid_2_kid_1_x) welcome_kid_2_kid_3_width)))
 (let ((?x2211 (+ (+ (+ ?x2208 welcome_kid_2_kid_0_x) welcome_kid_2_kid_0_width) welcome_kid_2_kid_4_x)))
 (let (($x2213 (or $x2001 (= ?x2211 0.0))))
 (let ((?x2039 (- welcome_kid_2_kid_2_x)))
 (let ((?x2114 (+ ?x2039 welcome_kid_2_kid_3_x)))
 (let ((?x2203 (+ (- (- ?x2114 welcome_kid_2_kid_1_x) welcome_kid_2_kid_2_width) welcome_kid_2_kid_0_x)))
 (let (($x2206 (or $x2001 (= (+ ?x2203 welcome_kid_2_kid_0_width) 0.0))))
 (let ((?x2196 (+ (- welcome_kid_2_kid_2_x (* 2.0 welcome_kid_2_kid_1_x)) welcome_kid_2_kid_0_x)))
 (let (($x2199 (= (+ (- ?x2196 welcome_kid_2_kid_1_width) welcome_kid_2_kid_0_width) 0.0)))
 (let (($x2200 (or $x2001 $x2199)))
 (let (($x2193 (= (+ (- welcome_kid_2_kid_4_width) welcome_kid_2_kid_0_width) 0.0)))
 (let (($x2191 (= (+ (- welcome_kid_2_kid_3_width) welcome_kid_2_kid_0_width) 0.0)))
 (let (($x2188 (= (+ (- welcome_kid_2_kid_2_width) welcome_kid_2_kid_0_width) 0.0)))
 (let (($x2185 (or $x2001 (= welcome_kid_2_kid_5_width 20.0))))
 (let (($x2183 (or $x2001 (= welcome_kid_2_kid_1_width 20.0))))
 (let ((?x2123 (- (+ (- welcome_kid_2_kid_4_width) welcome_kid_2_kid_5_x) welcome_kid_2_kid_4_x)))
 (let (($x2181 (or $x2001 (= ?x2123 10.0))))
 (let ((?x2119 (+ (- (- welcome_kid_2_kid_3_x) welcome_kid_2_kid_3_width) welcome_kid_2_kid_4_x)))
 (let (($x2179 (or $x2001 (= ?x2119 10.0))))
 (let (($x2177 (or $x2001 (= (- ?x2114 welcome_kid_2_kid_2_width) 10.0))))
 (let ((?x2111 (- (- welcome_kid_2_kid_2_x welcome_kid_2_kid_1_x) welcome_kid_2_kid_1_width)))
 (let (($x2175 (or $x2001 (= ?x2111 10.0))))
 (let ((?x2107 (- (- welcome_kid_2_kid_1_x welcome_kid_2_kid_0_x) welcome_kid_2_kid_0_width)))
 (let (($x2173 (or $x2001 (= ?x2107 10.0))))
 (let ((?x2168 (- (+ welcome_kid_2_kid_5_y welcome_kid_2_kid_5_hight) welcome_kid_2_y)))
 (let (($x2171 (or $x2001 (= (- ?x2168 welcome_kid_2_hight) (- 10.0)))))
 (let ((?x2163 (- (+ welcome_kid_2_kid_4_y welcome_kid_2_kid_4_hight) welcome_kid_2_y)))
 (let (($x2166 (or $x2001 (= (- ?x2163 welcome_kid_2_hight) (- 10.0)))))
 (let ((?x2063 (- welcome_kid_2_kid_3_y welcome_kid_2_y)))
 (let (($x2161 (or $x2001 (= (- (+ ?x2063 welcome_kid_2_kid_3_hight) welcome_kid_2_hight) (- 10.0)))))
 (let ((?x2045 (- welcome_kid_2_kid_2_y welcome_kid_2_y)))
 (let (($x2157 (or $x2001 (= (- (+ ?x2045 welcome_kid_2_kid_2_hight) welcome_kid_2_hight) (- 10.0)))))
 (let ((?x2150 (+ (- welcome_kid_2_kid_1_hight welcome_kid_2_y) welcome_kid_2_kid_1_y)))
 (let (($x2153 (or $x2001 (= (- ?x2150 welcome_kid_2_hight) (- 10.0)))))
 (let ((?x2145 (- (+ welcome_kid_2_kid_0_y welcome_kid_2_kid_0_hight) welcome_kid_2_y)))
 (let (($x2148 (or $x2001 (= (- ?x2145 welcome_kid_2_hight) (- 10.0)))))
 (let (($x2143 (or $x2001 (= (- welcome_kid_2_kid_5_y welcome_kid_2_y) 10.0))))
 (let (($x2141 (or $x2001 (= (- welcome_kid_2_kid_4_y welcome_kid_2_y) 10.0))))
 (let (($x2139 (or $x2001 (= ?x2063 10.0))))
 (let (($x2137 (or $x2001 (= ?x2045 10.0))))
 (let (($x2135 (or $x2001 (= (+ (- welcome_kid_2_y) welcome_kid_2_kid_1_y) 10.0))))
 (let (($x2133 (or $x2001 (= (- welcome_kid_2_kid_0_y welcome_kid_2_y) 10.0))))
 (let ((?x1578 (- welcome_kid_2_x)))
 (let ((?x1579 (- ?x1578 welcome_kid_2_width)))
 (let (($x2130 (= (+ (+ ?x1579 welcome_kid_2_kid_5_x) welcome_kid_2_kid_5_width) (- 10.0))))
 (let (($x2131 (or $x2001 $x2130)))
 (let (($x2127 (or $x2001 (= (+ ?x1578 welcome_kid_2_kid_0_x) 10.0))))
 (let (($x2125 (or $x2001 (>= ?x2123 0.0))))
 (let (($x2121 (or $x2001 (>= ?x2119 0.0))))
 (let (($x2117 (or $x2001 (>= (- ?x2114 welcome_kid_2_kid_2_width) 0.0))))
 (let (($x2113 (or $x2001 (>= ?x2111 0.0))))
 (let (($x2109 (or $x2001 (>= ?x2107 0.0))))
 (let ((?x2102 (+ (- (- welcome_kid_2_kid_5_y) welcome_kid_2_kid_5_hight) welcome_kid_2_y)))
 (let (($x2105 (or $x2001 (>= (+ ?x2102 welcome_kid_2_hight) 0.0))))
 (let (($x2099 (or $x2001 (>= (- welcome_kid_2_kid_5_y welcome_kid_2_y) 0.0))))
 (let ((?x2094 (- (- (+ welcome_kid_2_x welcome_kid_2_width) welcome_kid_2_kid_5_x) welcome_kid_2_kid_5_width)))
 (let (($x2096 (or $x2001 (>= ?x2094 0.0))))
 (let (($x2092 (or $x2001 (>= (+ ?x1578 welcome_kid_2_kid_5_x) 0.0))))
 (let ((?x2086 (+ (- (- welcome_kid_2_kid_4_y) welcome_kid_2_kid_4_hight) welcome_kid_2_y)))
 (let (($x2089 (or $x2001 (>= (+ ?x2086 welcome_kid_2_hight) 0.0))))
 (let (($x2083 (or $x2001 (>= (- welcome_kid_2_kid_4_y welcome_kid_2_y) 0.0))))
 (let ((?x2077 (+ (+ (- welcome_kid_2_kid_4_width) welcome_kid_2_x) welcome_kid_2_width)))
 (let (($x2080 (or $x2001 (>= (- ?x2077 welcome_kid_2_kid_4_x) 0.0))))
 (let (($x2074 (or $x2001 (>= (+ ?x1578 welcome_kid_2_kid_4_x) 0.0))))
 (let ((?x2068 (- (+ (- welcome_kid_2_kid_3_y) welcome_kid_2_y) welcome_kid_2_kid_3_hight)))
 (let (($x2071 (or $x2001 (>= (+ ?x2068 welcome_kid_2_hight) 0.0))))
 (let (($x2065 (or $x2001 (>= ?x2063 0.0))))
 (let ((?x2059 (- (+ (- welcome_kid_2_kid_3_x) welcome_kid_2_x) welcome_kid_2_kid_3_width)))
 (let (($x2062 (or $x2001 (>= (+ ?x2059 welcome_kid_2_width) 0.0))))
 (let (($x2056 (or $x2001 (>= (- welcome_kid_2_kid_3_x welcome_kid_2_x) 0.0))))
 (let ((?x2050 (- (+ (- welcome_kid_2_kid_2_y) welcome_kid_2_y) welcome_kid_2_kid_2_hight)))
 (let (($x2053 (or $x2001 (>= (+ ?x2050 welcome_kid_2_hight) 0.0))))
 (let (($x2047 (or $x2001 (>= ?x2045 0.0))))
 (let ((?x2042 (+ (- (+ ?x2039 welcome_kid_2_x) welcome_kid_2_kid_2_width) welcome_kid_2_width)))
 (let (($x2044 (or $x2001 (>= ?x2042 0.0))))
 (let (($x2038 (or $x2001 (>= (- welcome_kid_2_kid_2_x welcome_kid_2_x) 0.0))))
 (let ((?x2032 (- (+ (- welcome_kid_2_kid_1_hight) welcome_kid_2_y) welcome_kid_2_kid_1_y)))
 (let (($x2035 (or $x2001 (>= (+ ?x2032 welcome_kid_2_hight) 0.0))))
 (let (($x2029 (or $x2001 (>= (+ (- welcome_kid_2_y) welcome_kid_2_kid_1_y) 0.0))))
 (let ((?x2023 (- (+ (- welcome_kid_2_x welcome_kid_2_kid_1_x) welcome_kid_2_width) welcome_kid_2_kid_1_width)))
 (let (($x2025 (or $x2001 (>= ?x2023 0.0))))
 (let (($x2020 (or $x2001 (>= (+ ?x1578 welcome_kid_2_kid_1_x) 0.0))))
 (let ((?x2014 (+ (- (- welcome_kid_2_kid_0_y) welcome_kid_2_kid_0_hight) welcome_kid_2_y)))
 (let (($x2017 (or $x2001 (>= (+ ?x2014 welcome_kid_2_hight) 0.0))))
 (let (($x2011 (or $x2001 (>= (- welcome_kid_2_kid_0_y welcome_kid_2_y) 0.0))))
 (let ((?x2006 (- (- (+ welcome_kid_2_x welcome_kid_2_width) welcome_kid_2_kid_0_x) welcome_kid_2_kid_0_width)))
 (let (($x2008 (or $x2001 (>= ?x2006 0.0))))
 (let (($x2004 (or $x2001 (>= (+ ?x1578 welcome_kid_2_kid_0_x) 0.0))))
 (let (($x2000 (>= welcome_kid_2_kid_5_hight 0.0)))
 (let (($x1999 (>= welcome_kid_2_kid_5_width 0.0)))
 (let (($x1998 (>= welcome_kid_2_kid_5_y 0.0)))
 (let (($x1997 (>= welcome_kid_2_kid_5_x 0.0)))
 (let (($x1996 (>= welcome_kid_2_kid_4_hight 0.0)))
 (let (($x1995 (>= welcome_kid_2_kid_4_width 0.0)))
 (let (($x1994 (>= welcome_kid_2_kid_4_y 0.0)))
 (let (($x1993 (>= welcome_kid_2_kid_4_x 0.0)))
 (let (($x1992 (>= welcome_kid_2_kid_3_hight 0.0)))
 (let (($x1991 (>= welcome_kid_2_kid_3_width 0.0)))
 (let (($x1990 (>= welcome_kid_2_kid_3_y 0.0)))
 (let (($x1989 (>= welcome_kid_2_kid_3_x 0.0)))
 (let (($x1988 (>= welcome_kid_2_kid_2_hight 0.0)))
 (let (($x1987 (>= welcome_kid_2_kid_2_width 0.0)))
 (let (($x1986 (>= welcome_kid_2_kid_2_y 0.0)))
 (let (($x1985 (>= welcome_kid_2_kid_2_x 0.0)))
 (let (($x1984 (>= welcome_kid_2_kid_1_hight 0.0)))
 (let (($x1983 (>= welcome_kid_2_kid_1_width 0.0)))
 (let (($x1982 (>= welcome_kid_2_kid_1_y 0.0)))
 (let (($x1981 (>= welcome_kid_2_kid_1_x 0.0)))
 (let (($x1980 (>= welcome_kid_2_kid_0_hight 0.0)))
 (let (($x1979 (>= welcome_kid_2_kid_0_width 0.0)))
 (let (($x1978 (>= welcome_kid_2_kid_0_y 0.0)))
 (let (($x1977 (>= welcome_kid_2_kid_0_x 0.0)))
 (let ((?x1971 (+ (+ (- welcome_kid_1_kid_1_x) welcome_kid_1_kid_0_x) welcome_kid_1_kid_5_x)))
 (let ((?x1974 (- (- (+ ?x1971 welcome_kid_1_kid_0_width) welcome_kid_1_kid_4_x) welcome_kid_1_kid_4_width)))
 (let (($x1976 (or $x1760 (= ?x1974 0.0))))
 (let ((?x1964 (+ (- (- welcome_kid_1_kid_1_x) welcome_kid_1_kid_3_width) welcome_kid_1_kid_0_x)))
 (let ((?x1967 (- (+ (+ ?x1964 welcome_kid_1_kid_0_width) welcome_kid_1_kid_4_x) welcome_kid_1_kid_3_x)))
 (let (($x1969 (or $x1760 (= ?x1967 0.0))))
 (let ((?x1957 (+ (- (- welcome_kid_1_kid_1_x) welcome_kid_1_kid_2_x) welcome_kid_1_kid_0_x)))
 (let ((?x1960 (+ (+ (- ?x1957 welcome_kid_1_kid_2_width) welcome_kid_1_kid_0_width) welcome_kid_1_kid_3_x)))
 (let (($x1962 (or $x1760 (= ?x1960 0.0))))
 (let ((?x1951 (+ (+ (* (- 2.0) welcome_kid_1_kid_1_x) welcome_kid_1_kid_2_x) welcome_kid_1_kid_0_x)))
 (let (($x1954 (= (+ (- ?x1951 welcome_kid_1_kid_1_width) welcome_kid_1_kid_0_width) 0.0)))
 (let (($x1955 (or $x1760 $x1954)))
 (let (($x1948 (= (- welcome_kid_1_kid_0_width welcome_kid_1_kid_4_width) 0.0)))
 (let (($x1946 (= (+ (- welcome_kid_1_kid_3_width) welcome_kid_1_kid_0_width) 0.0)))
 (let (($x1944 (= (+ (- welcome_kid_1_kid_2_width) welcome_kid_1_kid_0_width) 0.0)))
 (let (($x1941 (or $x1760 (= welcome_kid_1_kid_5_width 20.0))))
 (let (($x1939 (or $x1760 (= welcome_kid_1_kid_1_width 20.0))))
 (let ((?x1879 (- (- welcome_kid_1_kid_5_x welcome_kid_1_kid_4_x) welcome_kid_1_kid_4_width)))
 (let (($x1937 (or $x1760 (= ?x1879 10.0))))
 (let ((?x1875 (- (+ (- welcome_kid_1_kid_3_width) welcome_kid_1_kid_4_x) welcome_kid_1_kid_3_x)))
 (let (($x1935 (or $x1760 (= ?x1875 10.0))))
 (let ((?x1870 (+ (- (- welcome_kid_1_kid_2_x) welcome_kid_1_kid_2_width) welcome_kid_1_kid_3_x)))
 (let (($x1933 (or $x1760 (= ?x1870 10.0))))
 (let ((?x1865 (- (+ (- welcome_kid_1_kid_1_x) welcome_kid_1_kid_2_x) welcome_kid_1_kid_1_width)))
 (let (($x1931 (or $x1760 (= ?x1865 10.0))))
 (let ((?x1860 (- (- welcome_kid_1_kid_1_x welcome_kid_1_kid_0_x) welcome_kid_1_kid_0_width)))
 (let (($x1929 (or $x1760 (= ?x1860 10.0))))
 (let ((?x1924 (- (+ welcome_kid_1_kid_5_y welcome_kid_1_kid_5_hight) welcome_kid_1_y)))
 (let (($x1927 (or $x1760 (= (- ?x1924 welcome_kid_1_hight) (- 10.0)))))
 (let ((?x1919 (- (+ welcome_kid_1_kid_4_y welcome_kid_1_kid_4_hight) welcome_kid_1_y)))
 (let (($x1922 (or $x1760 (= (- ?x1919 welcome_kid_1_hight) (- 10.0)))))
 (let ((?x1818 (- welcome_kid_1_kid_3_y welcome_kid_1_y)))
 (let (($x1917 (or $x1760 (= (- (+ ?x1818 welcome_kid_1_kid_3_hight) welcome_kid_1_hight) (- 10.0)))))
 (let ((?x1910 (+ (- welcome_kid_1_kid_2_hight welcome_kid_1_y) welcome_kid_1_kid_2_y)))
 (let (($x1913 (or $x1760 (= (- ?x1910 welcome_kid_1_hight) (- 10.0)))))
 (let ((?x1495 (- welcome_kid_1_y)))
 (let ((?x1785 (+ ?x1495 welcome_kid_1_kid_1_y)))
 (let (($x1908 (or $x1760 (= (+ (- ?x1785 welcome_kid_1_hight) welcome_kid_1_kid_1_hight) (- 10.0)))))
 (let ((?x1902 (+ (- (- welcome_kid_1_kid_0_hight welcome_kid_1_y) welcome_kid_1_hight) welcome_kid_1_kid_0_y)))
 (let (($x1904 (or $x1760 (= ?x1902 (- 10.0)))))
 (let (($x1899 (or $x1760 (= (- welcome_kid_1_kid_5_y welcome_kid_1_y) 10.0))))
 (let (($x1897 (or $x1760 (= (- welcome_kid_1_kid_4_y welcome_kid_1_y) 10.0))))
 (let (($x1895 (or $x1760 (= ?x1818 10.0))))
 (let (($x1893 (or $x1760 (= (+ ?x1495 welcome_kid_1_kid_2_y) 10.0))))
 (let (($x1891 (or $x1760 (= ?x1785 10.0))))
 (let (($x1889 (or $x1760 (= (+ ?x1495 welcome_kid_1_kid_0_y) 10.0))))
 (let ((?x1562 (- welcome_kid_1_x)))
 (let ((?x1563 (- ?x1562 welcome_kid_1_width)))
 (let (($x1886 (= (+ (+ ?x1563 welcome_kid_1_kid_5_x) welcome_kid_1_kid_5_width) (- 10.0))))
 (let (($x1887 (or $x1760 $x1886)))
 (let (($x1883 (or $x1760 (= (+ ?x1562 welcome_kid_1_kid_0_x) 10.0))))
 (let (($x1881 (or $x1760 (>= ?x1879 0.0))))
 (let (($x1877 (or $x1760 (>= ?x1875 0.0))))
 (let (($x1872 (or $x1760 (>= ?x1870 0.0))))
 (let (($x1867 (or $x1760 (>= ?x1865 0.0))))
 (let (($x1862 (or $x1760 (>= ?x1860 0.0))))
 (let ((?x1855 (+ (- (- welcome_kid_1_kid_5_y) welcome_kid_1_kid_5_hight) welcome_kid_1_y)))
 (let (($x1858 (or $x1760 (>= (+ ?x1855 welcome_kid_1_hight) 0.0))))
 (let (($x1852 (or $x1760 (>= (- welcome_kid_1_kid_5_y welcome_kid_1_y) 0.0))))
 (let ((?x1847 (- (- (+ welcome_kid_1_x welcome_kid_1_width) welcome_kid_1_kid_5_x) welcome_kid_1_kid_5_width)))
 (let (($x1849 (or $x1760 (>= ?x1847 0.0))))
 (let (($x1845 (or $x1760 (>= (+ ?x1562 welcome_kid_1_kid_5_x) 0.0))))
 (let ((?x1839 (+ (- (- welcome_kid_1_kid_4_y) welcome_kid_1_kid_4_hight) welcome_kid_1_y)))
 (let (($x1842 (or $x1760 (>= (+ ?x1839 welcome_kid_1_hight) 0.0))))
 (let (($x1836 (or $x1760 (>= (- welcome_kid_1_kid_4_y welcome_kid_1_y) 0.0))))
 (let ((?x1831 (- (- (+ welcome_kid_1_x welcome_kid_1_width) welcome_kid_1_kid_4_x) welcome_kid_1_kid_4_width)))
 (let (($x1833 (or $x1760 (>= ?x1831 0.0))))
 (let (($x1829 (or $x1760 (>= (+ ?x1562 welcome_kid_1_kid_4_x) 0.0))))
 (let ((?x1823 (- (+ (- welcome_kid_1_kid_3_y) welcome_kid_1_y) welcome_kid_1_kid_3_hight)))
 (let (($x1826 (or $x1760 (>= (+ ?x1823 welcome_kid_1_hight) 0.0))))
 (let (($x1820 (or $x1760 (>= ?x1818 0.0))))
 (let ((?x1815 (- (+ (- welcome_kid_1_x welcome_kid_1_kid_3_width) welcome_kid_1_width) welcome_kid_1_kid_3_x)))
 (let (($x1817 (or $x1760 (>= ?x1815 0.0))))
 (let (($x1812 (or $x1760 (>= (+ ?x1562 welcome_kid_1_kid_3_x) 0.0))))
 (let ((?x1806 (- (+ (- welcome_kid_1_kid_2_hight) welcome_kid_1_y) welcome_kid_1_kid_2_y)))
 (let (($x1809 (or $x1760 (>= (+ ?x1806 welcome_kid_1_hight) 0.0))))
 (let (($x1803 (or $x1760 (>= (+ ?x1495 welcome_kid_1_kid_2_y) 0.0))))
 (let ((?x1798 (- (+ (- welcome_kid_1_x welcome_kid_1_kid_2_x) welcome_kid_1_width) welcome_kid_1_kid_2_width)))
 (let (($x1800 (or $x1760 (>= ?x1798 0.0))))
 (let (($x1795 (or $x1760 (>= (+ ?x1562 welcome_kid_1_kid_2_x) 0.0))))
 (let ((?x1790 (- (+ (- welcome_kid_1_y welcome_kid_1_kid_1_y) welcome_kid_1_hight) welcome_kid_1_kid_1_hight)))
 (let (($x1792 (or $x1760 (>= ?x1790 0.0))))
 (let (($x1787 (or $x1760 (>= ?x1785 0.0))))
 (let ((?x1782 (- (+ (- welcome_kid_1_x welcome_kid_1_kid_1_x) welcome_kid_1_width) welcome_kid_1_kid_1_width)))
 (let (($x1784 (or $x1760 (>= ?x1782 0.0))))
 (let (($x1779 (or $x1760 (>= (+ ?x1562 welcome_kid_1_kid_1_x) 0.0))))
 (let ((?x1773 (+ (+ (- welcome_kid_1_kid_0_hight) welcome_kid_1_y) welcome_kid_1_hight)))
 (let (($x1776 (or $x1760 (>= (- ?x1773 welcome_kid_1_kid_0_y) 0.0))))
 (let (($x1770 (or $x1760 (>= (+ ?x1495 welcome_kid_1_kid_0_y) 0.0))))
 (let ((?x1765 (- (- (+ welcome_kid_1_x welcome_kid_1_width) welcome_kid_1_kid_0_x) welcome_kid_1_kid_0_width)))
 (let (($x1767 (or $x1760 (>= ?x1765 0.0))))
 (let (($x1763 (or $x1760 (>= (+ ?x1562 welcome_kid_1_kid_0_x) 0.0))))
 (let (($x1759 (>= welcome_kid_1_kid_5_hight 0.0)))
 (let (($x1758 (>= welcome_kid_1_kid_5_width 0.0)))
 (let (($x1757 (>= welcome_kid_1_kid_5_y 0.0)))
 (let (($x1756 (>= welcome_kid_1_kid_5_x 0.0)))
 (let (($x1755 (>= welcome_kid_1_kid_4_hight 0.0)))
 (let (($x1754 (>= welcome_kid_1_kid_4_width 0.0)))
 (let (($x1753 (>= welcome_kid_1_kid_4_y 0.0)))
 (let (($x1752 (>= welcome_kid_1_kid_4_x 0.0)))
 (let (($x1751 (>= welcome_kid_1_kid_3_hight 0.0)))
 (let (($x1750 (>= welcome_kid_1_kid_3_width 0.0)))
 (let (($x1749 (>= welcome_kid_1_kid_3_y 0.0)))
 (let (($x1748 (>= welcome_kid_1_kid_3_x 0.0)))
 (let (($x1747 (>= welcome_kid_1_kid_2_hight 0.0)))
 (let (($x1746 (>= welcome_kid_1_kid_2_width 0.0)))
 (let (($x1745 (>= welcome_kid_1_kid_2_y 0.0)))
 (let (($x1744 (>= welcome_kid_1_kid_2_x 0.0)))
 (let (($x1743 (>= welcome_kid_1_kid_1_hight 0.0)))
 (let (($x1742 (>= welcome_kid_1_kid_1_width 0.0)))
 (let (($x1741 (>= welcome_kid_1_kid_1_y 0.0)))
 (let (($x1740 (>= welcome_kid_1_kid_1_x 0.0)))
 (let (($x1739 (>= welcome_kid_1_kid_0_hight 0.0)))
 (let (($x1738 (>= welcome_kid_1_kid_0_width 0.0)))
 (let (($x1737 (>= welcome_kid_1_kid_0_y 0.0)))
 (let (($x1736 (>= welcome_kid_1_kid_0_x 0.0)))
 (let ((?x1701 (+ (- (- welcome_kid_0_kid_1_width) welcome_kid_0_kid_1_x) welcome_kid_0_kid_2_x)))
 (let (($x1735 (or $x1639 (= ?x1701 10.0))))
 (let ((?x1697 (- (- welcome_kid_0_kid_1_x welcome_kid_0_kid_0_x) welcome_kid_0_kid_0_width)))
 (let (($x1733 (or $x1639 (= ?x1697 10.0))))
 (let ((?x1728 (+ (+ (- welcome_kid_0_hight) welcome_kid_0_kid_2_y) welcome_kid_0_kid_2_hight)))
 (let (($x1731 (or $x1639 (= (- ?x1728 welcome_kid_0_y) (- 10.0)))))
 (let ((?x1723 (+ (- welcome_kid_0_kid_1_y welcome_kid_0_hight) welcome_kid_0_kid_1_hight)))
 (let (($x1726 (or $x1639 (= (- ?x1723 welcome_kid_0_y) (- 10.0)))))
 (let ((?x1718 (+ (+ (- welcome_kid_0_hight) welcome_kid_0_kid_0_y) welcome_kid_0_kid_0_hight)))
 (let (($x1721 (or $x1639 (= (- ?x1718 welcome_kid_0_y) (- 10.0)))))
 (let (($x1716 (or $x1639 (= (- welcome_kid_0_kid_2_y welcome_kid_0_y) 10.0))))
 (let (($x1714 (or $x1639 (= (- welcome_kid_0_kid_1_y welcome_kid_0_y) 10.0))))
 (let (($x1712 (or $x1639 (= (- welcome_kid_0_kid_0_y welcome_kid_0_y) 10.0))))
 (let ((?x1707 (+ (- (- welcome_kid_0_x) welcome_kid_0_width) welcome_kid_0_kid_2_x)))
 (let (($x1710 (or $x1639 (= (+ ?x1707 welcome_kid_0_kid_2_width) (- 10.0)))))
 (let (($x1705 (or $x1639 (= (+ (- welcome_kid_0_x) welcome_kid_0_kid_0_x) 10.0))))
 (let (($x1703 (or $x1639 (>= ?x1701 0.0))))
 (let (($x1699 (or $x1639 (>= ?x1697 0.0))))
 (let ((?x1692 (- (- welcome_kid_0_hight welcome_kid_0_kid_2_y) welcome_kid_0_kid_2_hight)))
 (let (($x1695 (or $x1639 (>= (+ ?x1692 welcome_kid_0_y) 0.0))))
 (let (($x1690 (or $x1639 (>= (- welcome_kid_0_kid_2_y welcome_kid_0_y) 0.0))))
 (let ((?x1685 (- (- (+ welcome_kid_0_x welcome_kid_0_width) welcome_kid_0_kid_2_x) welcome_kid_0_kid_2_width)))
 (let (($x1687 (or $x1639 (>= ?x1685 0.0))))
 (let (($x1683 (or $x1639 (>= (+ (- welcome_kid_0_x) welcome_kid_0_kid_2_x) 0.0))))
 (let ((?x1677 (- (+ (- welcome_kid_0_kid_1_y) welcome_kid_0_hight) welcome_kid_0_kid_1_hight)))
 (let (($x1680 (or $x1639 (>= (+ ?x1677 welcome_kid_0_y) 0.0))))
 (let (($x1674 (or $x1639 (>= (- welcome_kid_0_kid_1_y welcome_kid_0_y) 0.0))))
 (let ((?x1668 (- (+ (- welcome_kid_0_kid_1_width) welcome_kid_0_x) welcome_kid_0_kid_1_x)))
 (let (($x1671 (or $x1639 (>= (+ ?x1668 welcome_kid_0_width) 0.0))))
 (let (($x1666 (or $x1639 (>= (+ (- welcome_kid_0_x) welcome_kid_0_kid_1_x) 0.0))))
 (let ((?x1660 (- (- welcome_kid_0_hight welcome_kid_0_kid_0_y) welcome_kid_0_kid_0_hight)))
 (let (($x1663 (or $x1639 (>= (+ ?x1660 welcome_kid_0_y) 0.0))))
 (let (($x1658 (or $x1639 (>= (- welcome_kid_0_kid_0_y welcome_kid_0_y) 0.0))))
 (let ((?x1653 (- (- (+ welcome_kid_0_x welcome_kid_0_width) welcome_kid_0_kid_0_x) welcome_kid_0_kid_0_width)))
 (let (($x1655 (or $x1639 (>= ?x1653 0.0))))
 (let (($x1650 (or $x1639 (>= (+ (- welcome_kid_0_x) welcome_kid_0_kid_0_x) 0.0))))
 (let (($x1647 (or $x1639 (= (+ (- welcome_kid_0_kid_2_width) welcome_kid_0_kid_0_width) 0.0))))
 (let (($x1643 (or $x1639 (= (+ (- welcome_kid_0_kid_1_width) welcome_kid_0_kid_0_width) 0.0))))
 (let (($x1638 (>= welcome_kid_0_kid_2_hight 0.0)))
 (let (($x1637 (>= welcome_kid_0_kid_2_width 0.0)))
 (let (($x1636 (>= welcome_kid_0_kid_2_y 0.0)))
 (let (($x1635 (>= welcome_kid_0_kid_2_x 0.0)))
 (let (($x1634 (>= welcome_kid_0_kid_1_hight 0.0)))
 (let (($x1633 (>= welcome_kid_0_kid_1_width 0.0)))
 (let (($x1632 (>= welcome_kid_0_kid_1_y 0.0)))
 (let (($x1631 (>= welcome_kid_0_kid_1_x 0.0)))
 (let (($x1630 (>= welcome_kid_0_kid_0_hight 0.0)))
 (let (($x1629 (>= welcome_kid_0_kid_0_width 0.0)))
 (let (($x1628 (>= welcome_kid_0_kid_0_y 0.0)))
 (let (($x1627 (>= welcome_kid_0_kid_0_x 0.0)))
 (let (($x1626 (= (+ (- 400.0) welcome_width) 0.0)))
 (let (($x1623 (or $x1329 (> pic_width 450.0))))
 (let (($x1620 (or $x1489 (= (- welcome_kid_0_hight welcome_kid_3_hight) 0.0))))
 (let (($x1617 (or $x1489 (= (- welcome_kid_0_hight welcome_kid_2_hight) 0.0))))
 (let (($x1614 (or $x1489 (= (- welcome_kid_0_hight welcome_kid_1_hight) 0.0))))
 (let ((?x1501 (- (- welcome_kid_3_y welcome_kid_2_y) welcome_kid_2_hight)))
 (let (($x1611 (or $x1489 (>= ?x1501 0.0))))
 (let (($x1609 (or $x1489 (>= (- (+ ?x1495 welcome_kid_2_y) welcome_kid_1_hight) 0.0))))
 (let ((?x1492 (- (+ (- welcome_kid_0_hight) welcome_kid_1_y) welcome_kid_0_y)))
 (let (($x1607 (or $x1489 (>= ?x1492 0.0))))
 (let ((?x1603 (- (- (+ welcome_y welcome_hight) welcome_kid_3_y) welcome_kid_3_hight)))
 (let (($x1605 (or $x1489 (>= ?x1603 0.0))))
 (let (($x1601 (or $x1489 (>= (+ (- welcome_y) welcome_kid_3_y) 0.0))))
 (let ((?x1596 (- (+ (+ (- welcome_kid_3_width) welcome_x) welcome_width) welcome_kid_3_x)))
 (let (($x1598 (or $x1489 (>= ?x1596 0.0))))
 (let (($x1592 (or $x1489 (>= (+ (- welcome_x) welcome_kid_3_x) 0.0))))
 (let ((?x1588 (- (- (+ welcome_y welcome_hight) welcome_kid_2_y) welcome_kid_2_hight)))
 (let (($x1590 (or $x1489 (>= ?x1588 0.0))))
 (let (($x1586 (or $x1489 (>= (+ (- welcome_y) welcome_kid_2_y) 0.0))))
 (let (($x1583 (or $x1489 (>= (+ (+ ?x1579 welcome_x) welcome_width) 0.0))))
 (let (($x1577 (or $x1489 (>= (- welcome_kid_2_x welcome_x) 0.0))))
 (let ((?x1573 (- (- (+ welcome_y welcome_hight) welcome_kid_1_y) welcome_kid_1_hight)))
 (let (($x1575 (or $x1489 (>= ?x1573 0.0))))
 (let (($x1570 (or $x1489 (>= (+ (- welcome_y) welcome_kid_1_y) 0.0))))
 (let (($x1567 (or $x1489 (>= (+ (+ ?x1563 welcome_x) welcome_width) 0.0))))
 (let (($x1561 (or $x1489 (>= (- welcome_kid_1_x welcome_x) 0.0))))
 (let ((?x1557 (- (+ (- welcome_y welcome_kid_0_hight) welcome_hight) welcome_kid_0_y)))
 (let (($x1559 (or $x1489 (>= ?x1557 0.0))))
 (let (($x1554 (or $x1489 (>= (+ (- welcome_y) welcome_kid_0_y) 0.0))))
 (let ((?x1550 (+ (- (+ (- welcome_kid_0_x) welcome_x) welcome_kid_0_width) welcome_width)))
 (let (($x1552 (or $x1489 (>= ?x1550 0.0))))
 (let (($x1546 (or $x1489 (>= (- welcome_kid_0_x welcome_x) 0.0))))
 (let ((?x1542 (+ (+ (- (- welcome_y) welcome_hight) welcome_kid_3_y) welcome_kid_3_hight)))
 (let (($x1544 (or $x1489 (= ?x1542 0.0))))
 (let (($x1539 (or $x1489 (= (+ (- welcome_y) welcome_kid_0_y) 0.0))))
 (let ((?x1533 (+ (- (- welcome_kid_3_width welcome_x) welcome_width) welcome_kid_3_x)))
 (let (($x1535 (or $x1489 (= ?x1533 0.0))))
 (let ((?x1528 (- (- (+ welcome_kid_2_x welcome_kid_2_width) welcome_x) welcome_width)))
 (let (($x1530 (or $x1489 (= ?x1528 0.0))))
 (let ((?x1523 (- (- (+ welcome_kid_1_x welcome_kid_1_width) welcome_x) welcome_width)))
 (let (($x1525 (or $x1489 (= ?x1523 0.0))))
 (let ((?x1518 (- (+ (- welcome_kid_0_x welcome_x) welcome_kid_0_width) welcome_width)))
 (let (($x1520 (or $x1489 (= ?x1518 0.0))))
 (let (($x1516 (or $x1489 (= (+ (- welcome_x) welcome_kid_3_x) 0.0))))
 (let (($x1512 (or $x1489 (= (- welcome_kid_2_x welcome_x) 0.0))))
 (let (($x1509 (or $x1489 (= (- welcome_kid_1_x welcome_x) 0.0))))
 (let (($x1506 (or $x1489 (= (- welcome_kid_0_x welcome_x) 0.0))))
 (let (($x1503 (or $x1489 (= ?x1501 0.0))))
 (let (($x1499 (or $x1489 (= (- (+ ?x1495 welcome_kid_2_y) welcome_kid_1_hight) 0.0))))
 (let (($x1494 (or $x1489 (= ?x1492 0.0))))
 (let (($x1488 (>= welcome_kid_3_hight 0.0)))
 (let (($x1487 (>= welcome_kid_3_width 0.0)))
 (let (($x1486 (>= welcome_kid_3_y 0.0)))
 (let (($x1485 (>= welcome_kid_3_x 0.0)))
 (let (($x1484 (>= welcome_kid_2_hight 0.0)))
 (let (($x1483 (>= welcome_kid_2_width 0.0)))
 (let (($x1482 (>= welcome_kid_2_y 0.0)))
 (let (($x1481 (>= welcome_kid_2_x 0.0)))
 (let (($x1480 (>= welcome_kid_1_hight 0.0)))
 (let (($x1479 (>= welcome_kid_1_width 0.0)))
 (let (($x1478 (>= welcome_kid_1_y 0.0)))
 (let (($x1477 (>= welcome_kid_1_x 0.0)))
 (let (($x1476 (>= welcome_kid_0_hight 0.0)))
 (let (($x1475 (>= welcome_kid_0_width 0.0)))
 (let (($x1474 (>= welcome_kid_0_y 0.0)))
 (let (($x1473 (>= welcome_kid_0_x 0.0)))
 (let (($x1472 (= (- pic_width pic_hight) 0.0)))
 (let (($x1470 (or $x1329 (= side_bar_width 300.0))))
 (let (($x1466 (= (- (+ (+ (- ads_hight) welcome_y) welcome_hight) ads_y) 0.0)))
 (let (($x1467 (or $x1329 $x1466)))
 (let (($x1462 (or $x1329 (= (- (+ (+ (- ads_hight) pic_y) pic_hight) ads_y) 0.0))))
 (let (($x1456 (= (- (+ (+ (- ads_hight) side_bar_y) side_bar_hight) ads_y) 0.0)))
 (let (($x1457 (or $x1329 $x1456)))
 (let (($x1451 (or $x1329 (= (- welcome_y ads_y) 0.0))))
 (let (($x1449 (or $x1329 (= (- pic_y ads_y) 0.0))))
 (let (($x1447 (or $x1329 (= (- side_bar_y ads_y) 0.0))))
 (let (($x1444 (= (+ (+ (- (- ads_x) ads_width) welcome_x) welcome_width) 0.0)))
 (let (($x1445 (or $x1329 $x1444)))
 (let (($x1440 (or $x1329 (= (+ (- ads_x) side_bar_x) 0.0))))
 (let (($x1438 (or $x1329 (= ?x1432 10.0))))
 (let (($x1436 (or $x1329 (= (- (+ (- side_bar_width) pic_x) side_bar_x) 10.0))))
 (let (($x1434 (or $x1329 $x1433)))
 (let (($x1430 (or $x1329 (>= (- (+ (- side_bar_width) pic_x) side_bar_x) 0.0))))
 (let (($x1426 (or $x1329 (>= (+ (- (- ads_hight welcome_y) welcome_hight) ads_y) 0.0))))
 (let (($x1421 (or $x1329 (>= (- welcome_y ads_y) 0.0))))
 (let (($x1418 (or $x1329 (>= (- (- (+ ads_x ads_width) welcome_x) welcome_width) 0.0))))
 (let (($x1413 (or $x1329 (>= (+ (- ads_x) welcome_x) 0.0))))
 (let (($x1410 (or $x1329 (>= (+ (- (- ads_hight pic_y) pic_hight) ads_y) 0.0))))
 (let (($x1405 (or $x1329 (>= (- pic_y ads_y) 0.0))))
 (let (($x1402 (or $x1329 (>= (- (+ (+ (- pic_width) ads_x) ads_width) pic_x) 0.0))))
 (let (($x1396 (or $x1329 (>= (+ (- ads_x) pic_x) 0.0))))
 (let (($x1392 (>= (+ (- (- ads_hight side_bar_y) side_bar_hight) ads_y) 0.0)))
 (let (($x1393 (or $x1329 $x1392)))
 (let (($x1388 (or $x1329 (>= (- side_bar_y ads_y) 0.0))))
 (let (($x1384 (>= (- (+ (+ (- side_bar_width) ads_x) ads_width) side_bar_x) 0.0)))
 (let (($x1385 (or $x1329 $x1384)))
 (let (($x1379 (or $x1329 (>= (+ (- ads_x) side_bar_x) 0.0))))
 (let (($x1375 (>= welcome_hight 0.0)))
 (let (($x1374 (>= welcome_width 0.0)))
 (let (($x1373 (>= welcome_y 0.0)))
 (let (($x1372 (>= welcome_x 0.0)))
 (let (($x1371 (>= pic_hight 0.0)))
 (let (($x1370 (>= pic_width 0.0)))
 (let (($x1369 (>= pic_y 0.0)))
 (let (($x1368 (>= pic_x 0.0)))
 (let (($x1367 (>= side_bar_hight 0.0)))
 (let (($x1366 (>= side_bar_width 0.0)))
 (let (($x1365 (>= side_bar_y 0.0)))
 (let (($x1364 (>= side_bar_x 0.0)))
 (let (($x1363 (or $x1329 $x1345)))
 (let (($x1362 (or ads_feasible ads2_feasible)))
 (let (($x1360 (= (+ (+ (- (- ads_holder_y) ads_holder_hight) ads2_y) ads2_hight) 0.0)))
 (let (($x1361 (or $x1345 $x1360)))
 (let (($x1357 (or $x1345 (= (+ (- ads_holder_y) ads2_y) 0.0))))
 (let (($x1353 (= (+ (- (- ads2_width ads_holder_x) ads_holder_width) ads2_x) 0.0)))
 (let (($x1354 (or $x1345 $x1353)))
 (let (($x1349 (or $x1345 (= (+ (- ads_holder_x) ads2_x) 0.0))))
 (let (($x1343 (= (+ (- (+ (- ads_holder_y) ads_hight) ads_holder_hight) ads_y) 0.0)))
 (let (($x1344 (or $x1329 $x1343)))
 (let (($x1339 (or $x1329 (= (+ (- ads_holder_y) ads_y) 0.0))))
 (let (($x1335 (= (- (+ (- ads_x ads_holder_x) ads_width) ads_holder_width) 0.0)))
 (let (($x1336 (or $x1329 $x1335)))
 (let (($x1332 (or $x1329 (= (- ads_x ads_holder_x) 0.0))))
 (let (($x1328 (>= ads2_hight 0.0)))
 (let (($x1327 (>= ads2_width 0.0)))
 (let (($x1326 (>= ads2_y 0.0)))
 (let (($x1325 (>= ads2_x 0.0)))
 (let (($x1324 (>= ads_hight 0.0)))
 (let (($x1323 (>= ads_width 0.0)))
 (let (($x1322 (>= ads_y 0.0)))
 (let (($x1321 (>= ads_x 0.0)))
 (let (($x1314 (> back_ground_width 1200.0)))
 (let (($x1320 (or $x1314 (= (- back_ground_width main_body_width) 0.0))))
 (let (($x1316 (= main_body_width 1200.0)))
 (let (($x1317 (or (not $x1314) $x1316)))
 (let ((?x1309 (* 2.0 back_ground_x)))
 (let ((?x1311 (+ (- (+ (- back_ground_width) (* 2.0 main_body_x)) ?x1309) main_body_width)))
 (let (($x1312 (= ?x1311 0.0)))
 (let ((?x1305 (+ (- (+ (- main_body_y) recommend_hight) main_body_hight) recommend_y)))
 (let (($x1306 (= ?x1305 0.0)))
 (let ((?x1271 (- ads_holder_y main_body_y)))
 (let (($x1302 (= ?x1271 0.0)))
 (let ((?x1300 (- (+ (- recommend_x main_body_x) recommend_width) main_body_width)))
 (let (($x1301 (= ?x1300 0.0)))
 (let ((?x1297 (- (+ (+ (- main_body_x) ads_holder_x) ads_holder_width) main_body_width)))
 (let (($x1298 (= ?x1297 0.0)))
 (let ((?x1278 (- recommend_x main_body_x)))
 (let (($x1295 (= ?x1278 0.0)))
 (let ((?x1265 (+ (- main_body_x) ads_holder_x)))
 (let (($x1294 (= ?x1265 0.0)))
 (let (($x1293 (>= (+ (- (- ads_holder_y) ads_holder_hight) recommend_y) 0.0)))
 (let ((?x1289 (- (+ (- main_body_y recommend_hight) main_body_hight) recommend_y)))
 (let (($x1290 (>= ?x1289 0.0)))
 (let (($x1286 (>= (+ (- main_body_y) recommend_y) 0.0)))
 (let (($x1284 (>= (+ (- (+ ?x1280 main_body_x) recommend_width) main_body_width) 0.0)))
 (let (($x1279 (>= ?x1278 0.0)))
 (let ((?x1276 (+ (- (+ (- ads_holder_y) main_body_y) ads_holder_hight) main_body_hight)))
 (let (($x1277 (>= ?x1276 0.0)))
 (let (($x1272 (>= ?x1271 0.0)))
 (let ((?x1269 (+ (- (- main_body_x ads_holder_x) ads_holder_width) main_body_width)))
 (let (($x1270 (>= ?x1269 0.0)))
 (let (($x1266 (>= ?x1265 0.0)))
 (let (($x1263 (>= recommend_hight 0.0)))
 (let (($x1262 (>= recommend_width 0.0)))
 (let (($x1261 (>= recommend_y 0.0)))
 (let (($x1260 (>= recommend_x 0.0)))
 (let (($x1259 (>= ads_holder_hight 0.0)))
 (let (($x1258 (>= ads_holder_width 0.0)))
 (let (($x1257 (>= ads_holder_y 0.0)))
 (let (($x1256 (>= ads_holder_x 0.0)))
 (let (($x1255 (= (+ (- 150.0) cart_width) 0.0)))
 (let (($x1253 (= (+ (- (- (- 100.0) search_icon_width) search_icon_x) cart_x) 0.0)))
 (let (($x1249 (= (+ (- cart_hight) search_box_hight) 0.0)))
 (let (($x1246 (= (+ (- cart_y) search_box_y) 0.0)))
 (let (($x1243 (>= cart_hight 0.0)))
 (let (($x1242 (>= cart_width 0.0)))
 (let (($x1241 (>= cart_y 0.0)))
 (let (($x1240 (>= cart_x 0.0)))
 (let (($x1239 (= (+ (- 50.0) search_icon_width) 0.0)))
 (let (($x1237 (= (- (- search_icon_x search_box_x) search_box_width) 0.0)))
 (let (($x1234 (= (- search_box_hight search_icon_hight) 0.0)))
 (let (($x1232 (= (- search_box_y search_icon_y) 0.0)))
 (let (($x1230 (>= search_icon_hight 0.0)))
 (let (($x1229 (>= search_icon_width 0.0)))
 (let (($x1228 (>= search_icon_y 0.0)))
 (let (($x1227 (>= search_icon_x 0.0)))
 (let (($x1226 (= (+ (- back_ground_width) (* 2.0 search_box_width)) 0.0)))
 (let (($x1223 (= (+ (- 50.0) search_box_hight) 0.0)))
 (let ((?x1218 (- (+ (* (- 2.0) title_bg_x) (* 2.0 search_box_x)) title_bg_width)))
 (let (($x1220 (= (+ ?x1218 search_box_width) 0.0)))
 (let ((?x1212 (- (+ (* (- 2.0) title_bg_y) (* 2.0 search_box_y)) title_bg_hight)))
 (let (($x1214 (= (+ ?x1212 search_box_hight) 0.0)))
 (let (($x1207 (>= search_box_hight 0.0)))
 (let (($x1206 (>= search_box_width 0.0)))
 (let (($x1205 (>= search_box_y 0.0)))
 (let (($x1204 (>= search_box_x 0.0)))
 (let ((?x1202 (- (- (+ search_buttons_y search_buttons_hight) title_bar_y) title_bar_hight)))
 (let (($x1203 (= ?x1202 0.0)))
 (let ((?x1134 (+ (- (- search_buttons_kid_4_x) search_buttons_kid_4_width) search_buttons_kid_5_x)))
 (let (($x1199 (= ?x1134 20.0)))
 (let ((?x1130 (- (+ (- search_buttons_kid_3_x) search_buttons_kid_4_x) search_buttons_kid_3_width)))
 (let (($x1198 (= ?x1130 20.0)))
 (let ((?x1126 (- (- search_buttons_kid_3_x search_buttons_kid_2_x) search_buttons_kid_2_width)))
 (let (($x1197 (= ?x1126 20.0)))
 (let ((?x1123 (- (- search_buttons_kid_2_x search_buttons_kid_1_x) search_buttons_kid_1_width)))
 (let (($x1196 (= ?x1123 20.0)))
 (let ((?x1120 (- (+ (- search_buttons_kid_0_width) search_buttons_kid_1_x) search_buttons_kid_0_x)))
 (let (($x1195 (= ?x1120 20.0)))
 (let ((?x992 (- search_buttons_y)))
 (let ((?x1112 (+ ?x992 search_buttons_kid_5_y)))
 (let (($x1194 (= (+ (- ?x1112 search_buttons_hight) search_buttons_kid_5_hight) (- 10.0))))
 (let ((?x1189 (- (- search_buttons_kid_4_hight search_buttons_y) search_buttons_hight)))
 (let (($x1191 (= (+ ?x1189 search_buttons_kid_4_y) (- 10.0))))
 (let ((?x1185 (- (- search_buttons_kid_3_hight search_buttons_y) search_buttons_hight)))
 (let (($x1187 (= (+ ?x1185 search_buttons_kid_3_y) (- 10.0))))
 (let ((?x1181 (- (+ search_buttons_kid_2_y search_buttons_kid_2_hight) search_buttons_y)))
 (let (($x1183 (= (- ?x1181 search_buttons_hight) (- 10.0))))
 (let ((?x1060 (- search_buttons_kid_1_y search_buttons_y)))
 (let (($x1179 (= (- (+ ?x1060 search_buttons_kid_1_hight) search_buttons_hight) (- 10.0))))
 (let ((?x1175 (+ (- (+ ?x992 search_buttons_kid_0_y) search_buttons_hight) search_buttons_kid_0_hight)))
 (let (($x1176 (= ?x1175 (- 10.0))))
 (let (($x1173 (= ?x1112 10.0)))
 (let ((?x1099 (+ ?x992 search_buttons_kid_4_y)))
 (let (($x1172 (= ?x1099 10.0)))
 (let ((?x1086 (+ ?x992 search_buttons_kid_3_y)))
 (let (($x1171 (= ?x1086 10.0)))
 (let ((?x1073 (- search_buttons_kid_2_y search_buttons_y)))
 (let (($x1170 (= ?x1073 10.0)))
 (let (($x1169 (= ?x1060 10.0)))
 (let ((?x1048 (+ ?x992 search_buttons_kid_0_y)))
 (let (($x1168 (= ?x1048 10.0)))
 (let ((?x1164 (- (+ (- search_buttons_width) search_buttons_kid_5_width) search_buttons_x)))
 (let (($x1167 (= (+ ?x1164 search_buttons_kid_5_x) (- 10.0))))
 (let ((?x1041 (- search_buttons_x)))
 (let ((?x1042 (+ ?x1041 search_buttons_kid_0_x)))
 (let (($x1162 (= ?x1042 10.0)))
 (let (($x1160 (= search_buttons_kid_0_hight 30.0)))
 (let (($x1158 (= (- search_buttons_kid_0_hight search_buttons_kid_5_hight) 0.0)))
 (let (($x1156 (= (+ (- search_buttons_kid_4_hight) search_buttons_kid_0_hight) 0.0)))
 (let (($x1154 (= (+ (- search_buttons_kid_3_hight) search_buttons_kid_0_hight) 0.0)))
 (let (($x1152 (= (+ (- search_buttons_kid_2_hight) search_buttons_kid_0_hight) 0.0)))
 (let (($x1149 (= (+ (- search_buttons_kid_1_hight) search_buttons_kid_0_hight) 0.0)))
 (let (($x1146 (= search_buttons_kid_0_width 100.0)))
 (let (($x1145 (= (- search_buttons_kid_0_width search_buttons_kid_5_width) 0.0)))
 (let (($x1143 (= (- search_buttons_kid_0_width search_buttons_kid_4_width) 0.0)))
 (let (($x1141 (= (- search_buttons_kid_0_width search_buttons_kid_3_width) 0.0)))
 (let (($x1139 (= (- search_buttons_kid_0_width search_buttons_kid_2_width) 0.0)))
 (let (($x1137 (= (- search_buttons_kid_0_width search_buttons_kid_1_width) 0.0)))
 (let (($x1135 (>= ?x1134 0.0)))
 (let (($x1131 (>= ?x1130 0.0)))
 (let (($x1127 (>= ?x1126 0.0)))
 (let (($x1124 (>= ?x1123 0.0)))
 (let (($x1121 (>= ?x1120 0.0)))
 (let ((?x1116 (- (+ (- search_buttons_y search_buttons_kid_5_y) search_buttons_hight) search_buttons_kid_5_hight)))
 (let (($x1117 (>= ?x1116 0.0)))
 (let (($x1113 (>= ?x1112 0.0)))
 (let ((?x1109 (+ (- search_buttons_width search_buttons_kid_5_width) search_buttons_x)))
 (let (($x1111 (>= (- ?x1109 search_buttons_kid_5_x) 0.0)))
 (let (($x1107 (>= (+ ?x1041 search_buttons_kid_5_x) 0.0)))
 (let ((?x1103 (+ (+ (- search_buttons_kid_4_hight) search_buttons_y) search_buttons_hight)))
 (let (($x1105 (>= (- ?x1103 search_buttons_kid_4_y) 0.0)))
 (let (($x1100 (>= ?x1099 0.0)))
 (let ((?x1096 (- (- search_buttons_width search_buttons_kid_4_x) search_buttons_kid_4_width)))
 (let (($x1098 (>= (+ ?x1096 search_buttons_x) 0.0)))
 (let (($x1094 (>= (- search_buttons_kid_4_x search_buttons_x) 0.0)))
 (let ((?x1090 (+ (+ (- search_buttons_kid_3_hight) search_buttons_y) search_buttons_hight)))
 (let (($x1092 (>= (- ?x1090 search_buttons_kid_3_y) 0.0)))
 (let (($x1087 (>= ?x1086 0.0)))
 (let ((?x1083 (- (- search_buttons_width search_buttons_kid_3_x) search_buttons_kid_3_width)))
 (let (($x1085 (>= (+ ?x1083 search_buttons_x) 0.0)))
 (let (($x1081 (>= (- search_buttons_kid_3_x search_buttons_x) 0.0)))
 (let ((?x1077 (+ (- (- search_buttons_kid_2_y) search_buttons_kid_2_hight) search_buttons_y)))
 (let (($x1079 (>= (+ ?x1077 search_buttons_hight) 0.0)))
 (let (($x1074 (>= ?x1073 0.0)))
 (let ((?x1070 (- (- search_buttons_width search_buttons_kid_2_x) search_buttons_kid_2_width)))
 (let (($x1072 (>= (+ ?x1070 search_buttons_x) 0.0)))
 (let (($x1068 (>= (- search_buttons_kid_2_x search_buttons_x) 0.0)))
 (let ((?x1064 (- (+ (- search_buttons_kid_1_y) search_buttons_y) search_buttons_kid_1_hight)))
 (let (($x1066 (>= (+ ?x1064 search_buttons_hight) 0.0)))
 (let (($x1061 (>= ?x1060 0.0)))
 (let ((?x1058 (- (+ (- search_buttons_width search_buttons_kid_1_x) search_buttons_x) search_buttons_kid_1_width)))
 (let (($x1059 (>= ?x1058 0.0)))
 (let (($x1055 (>= (- search_buttons_kid_1_x search_buttons_x) 0.0)))
 (let ((?x1052 (- (+ (- search_buttons_y search_buttons_kid_0_y) search_buttons_hight) search_buttons_kid_0_hight)))
 (let (($x1053 (>= ?x1052 0.0)))
 (let (($x1049 (>= ?x1048 0.0)))
 (let ((?x1045 (+ (- search_buttons_width search_buttons_kid_0_width) search_buttons_x)))
 (let (($x1047 (>= (- ?x1045 search_buttons_kid_0_x) 0.0)))
 (let (($x1043 (>= ?x1042 0.0)))
 (let (($x1040 (>= search_buttons_kid_5_hight 0.0)))
 (let (($x1039 (>= search_buttons_kid_5_width 0.0)))
 (let (($x1038 (>= search_buttons_kid_5_y 0.0)))
 (let (($x1037 (>= search_buttons_kid_5_x 0.0)))
 (let (($x1036 (>= search_buttons_kid_4_hight 0.0)))
 (let (($x1035 (>= search_buttons_kid_4_width 0.0)))
 (let (($x1034 (>= search_buttons_kid_4_y 0.0)))
 (let (($x1033 (>= search_buttons_kid_4_x 0.0)))
 (let (($x1032 (>= search_buttons_kid_3_hight 0.0)))
 (let (($x1031 (>= search_buttons_kid_3_width 0.0)))
 (let (($x1030 (>= search_buttons_kid_3_y 0.0)))
 (let (($x1029 (>= search_buttons_kid_3_x 0.0)))
 (let (($x1028 (>= search_buttons_kid_2_hight 0.0)))
 (let (($x1027 (>= search_buttons_kid_2_width 0.0)))
 (let (($x1026 (>= search_buttons_kid_2_y 0.0)))
 (let (($x1025 (>= search_buttons_kid_2_x 0.0)))
 (let (($x1024 (>= search_buttons_kid_1_hight 0.0)))
 (let (($x1023 (>= search_buttons_kid_1_width 0.0)))
 (let (($x1022 (>= search_buttons_kid_1_y 0.0)))
 (let (($x1021 (>= search_buttons_kid_1_x 0.0)))
 (let (($x1020 (>= search_buttons_kid_0_hight 0.0)))
 (let (($x1019 (>= search_buttons_kid_0_width 0.0)))
 (let (($x1018 (>= search_buttons_kid_0_y 0.0)))
 (let (($x1017 (>= search_buttons_kid_0_x 0.0)))
 (let ((?x969 (- icon_x title_bar_x)))
 (let (($x1016 (= ?x969 50.0)))
 (let ((?x1014 (- (+ (- (* 2.0 icon_y) (* 2.0 title_bar_y)) icon_hight) title_bar_hight)))
 (let (($x1015 (= ?x1014 0.0)))
 (let (($x1008 (= (+ (- 100.0) icon_hight) 0.0)))
 (let (($x1005 (= (+ (- 150.0) icon_width) 0.0)))
 (let ((?x998 (+ (- (- icon_x) icon_width) search_buttons_x)))
 (let (($x1002 (>= ?x998 50.0)))
 (let ((?x554 (- title_bar_x title_bg_x)))
 (let (($x555 (= ?x554 0.0)))
 (let (($x1001 (= title_bar_hight 200.0)))
 (let (($x999 (>= ?x998 0.0)))
 (let (($x996 (>= (+ (+ (- ?x992 search_buttons_hight) title_bar_y) title_bar_hight) 0.0)))
 (let (($x991 (>= (- search_buttons_y title_bar_y) 0.0)))
 (let ((?x988 (- (+ (+ (- search_buttons_width) title_bar_x) title_bar_width) search_buttons_x)))
 (let (($x989 (>= ?x988 0.0)))
 (let (($x984 (>= (+ (- title_bar_x) search_buttons_x) 0.0)))
 (let (($x982 (>= (+ (- (+ (- icon_y) title_bar_y) icon_hight) title_bar_hight) 0.0)))
 (let (($x977 (>= (- icon_y title_bar_y) 0.0)))
 (let (($x975 (>= (+ (- (+ (- icon_x) title_bar_x) icon_width) title_bar_width) 0.0)))
 (let (($x970 (>= ?x969 0.0)))
 (let (($x968 (>= search_buttons_hight 0.0)))
 (let (($x967 (>= search_buttons_width 0.0)))
 (let (($x966 (>= search_buttons_y 0.0)))
 (let (($x965 (>= search_buttons_x 0.0)))
 (let (($x964 (>= icon_hight 0.0)))
 (let (($x963 (>= icon_width 0.0)))
 (let (($x962 (>= icon_y 0.0)))
 (let (($x961 (>= icon_x 0.0)))
 (let ((?x959 (+ (- (- title_top_right_width title_top_x) title_top_width) title_top_right_x)))
 (let (($x960 (= ?x959 0.0)))
 (let ((?x570 (- title_top_x)))
 (let ((?x608 (+ ?x570 title_top_left_x)))
 (let (($x956 (= ?x608 0.0)))
 (let ((?x890 (- (+ (- title_top_right_kid_6_x) title_top_right_kid_7_x) title_top_right_kid_6_width)))
 (let (($x955 (= ?x890 0.0)))
 (let ((?x886 (- (- title_top_right_kid_6_x title_top_right_kid_5_x) title_top_right_kid_5_width)))
 (let (($x954 (= ?x886 0.0)))
 (let ((?x883 (- (- title_top_right_kid_5_x title_top_right_kid_4_x) title_top_right_kid_4_width)))
 (let (($x953 (= ?x883 0.0)))
 (let ((?x880 (- (+ (- title_top_right_kid_3_width) title_top_right_kid_4_x) title_top_right_kid_3_x)))
 (let (($x952 (= ?x880 0.0)))
 (let ((?x876 (+ (- (- title_top_right_kid_2_width) title_top_right_kid_2_x) title_top_right_kid_3_x)))
 (let (($x951 (= ?x876 0.0)))
 (let ((?x873 (+ (- (- title_top_right_kid_1_x) title_top_right_kid_1_width) title_top_right_kid_2_x)))
 (let (($x950 (= ?x873 0.0)))
 (let ((?x870 (- (- title_top_right_kid_1_x title_top_right_kid_0_x) title_top_right_kid_0_width)))
 (let (($x949 (= ?x870 0.0)))
 (let ((?x946 (- (- title_top_right_kid_7_hight title_top_right_y) title_top_right_hight)))
 (let (($x948 (= (+ ?x946 title_top_right_kid_7_y) 0.0)))
 (let ((?x942 (- (- title_top_right_kid_6_hight title_top_right_y) title_top_right_hight)))
 (let (($x944 (= (+ ?x942 title_top_right_kid_6_y) 0.0)))
 (let ((?x938 (- (+ title_top_right_kid_5_y title_top_right_kid_5_hight) title_top_right_y)))
 (let (($x940 (= (- ?x938 title_top_right_hight) 0.0)))
 (let ((?x823 (- title_top_right_kid_4_y title_top_right_y)))
 (let (($x936 (= (- (+ ?x823 title_top_right_kid_4_hight) title_top_right_hight) 0.0)))
 (let ((?x769 (- title_top_right_y)))
 (let ((?x811 (+ ?x769 title_top_right_kid_3_y)))
 (let (($x933 (= (+ (- ?x811 title_top_right_hight) title_top_right_kid_3_hight) 0.0)))
 (let ((?x797 (- title_top_right_kid_2_y title_top_right_y)))
 (let (($x930 (= (- (+ ?x797 title_top_right_kid_2_hight) title_top_right_hight) 0.0)))
 (let ((?x926 (+ (- (+ ?x769 title_top_right_kid_1_y) title_top_right_hight) title_top_right_kid_1_hight)))
 (let (($x927 (= ?x926 0.0)))
 (let ((?x922 (- (- title_top_right_kid_0_hight title_top_right_y) title_top_right_hight)))
 (let (($x924 (= (+ ?x922 title_top_right_kid_0_y) 0.0)))
 (let ((?x862 (+ ?x769 title_top_right_kid_7_y)))
 (let (($x920 (= ?x862 0.0)))
 (let ((?x849 (+ ?x769 title_top_right_kid_6_y)))
 (let (($x919 (= ?x849 0.0)))
 (let ((?x836 (- title_top_right_kid_5_y title_top_right_y)))
 (let (($x918 (= ?x836 0.0)))
 (let (($x917 (= ?x823 0.0)))
 (let (($x916 (= ?x811 0.0)))
 (let (($x915 (= ?x797 0.0)))
 (let ((?x784 (+ ?x769 title_top_right_kid_1_y)))
 (let (($x914 (= ?x784 0.0)))
 (let ((?x770 (+ ?x769 title_top_right_kid_0_y)))
 (let (($x913 (= ?x770 0.0)))
 (let ((?x910 (+ (+ (- title_top_right_width) title_top_right_kid_7_x) title_top_right_kid_7_width)))
 (let (($x912 (= (- ?x910 title_top_right_x) 0.0)))
 (let ((?x763 (- title_top_right_kid_0_x title_top_right_x)))
 (let (($x908 (= ?x763 0.0)))
 (let (($x907 (= title_top_right_kid_0_width 100.0)))
 (let (($x906 (= (- title_top_right_kid_0_width title_top_right_kid_7_width) 0.0)))
 (let (($x904 (= (- title_top_right_kid_0_width title_top_right_kid_6_width) 0.0)))
 (let (($x902 (= (- title_top_right_kid_0_width title_top_right_kid_5_width) 0.0)))
 (let (($x900 (= (- title_top_right_kid_0_width title_top_right_kid_4_width) 0.0)))
 (let (($x898 (= (+ (- title_top_right_kid_3_width) title_top_right_kid_0_width) 0.0)))
 (let (($x896 (= (+ (- title_top_right_kid_2_width) title_top_right_kid_0_width) 0.0)))
 (let (($x894 (= (+ (- title_top_right_kid_1_width) title_top_right_kid_0_width) 0.0)))
 (let (($x891 (>= ?x890 0.0)))
 (let (($x887 (>= ?x886 0.0)))
 (let (($x884 (>= ?x883 0.0)))
 (let (($x881 (>= ?x880 0.0)))
 (let (($x877 (>= ?x876 0.0)))
 (let (($x874 (>= ?x873 0.0)))
 (let (($x871 (>= ?x870 0.0)))
 (let ((?x866 (+ (+ (- title_top_right_kid_7_hight) title_top_right_y) title_top_right_hight)))
 (let (($x868 (>= (- ?x866 title_top_right_kid_7_y) 0.0)))
 (let (($x863 (>= ?x862 0.0)))
 (let ((?x859 (- (- title_top_right_width title_top_right_kid_7_x) title_top_right_kid_7_width)))
 (let (($x861 (>= (+ ?x859 title_top_right_x) 0.0)))
 (let (($x857 (>= (- title_top_right_kid_7_x title_top_right_x) 0.0)))
 (let ((?x853 (+ (+ (- title_top_right_kid_6_hight) title_top_right_y) title_top_right_hight)))
 (let (($x855 (>= (- ?x853 title_top_right_kid_6_y) 0.0)))
 (let (($x850 (>= ?x849 0.0)))
 (let ((?x846 (- (- title_top_right_width title_top_right_kid_6_x) title_top_right_kid_6_width)))
 (let (($x848 (>= (+ ?x846 title_top_right_x) 0.0)))
 (let (($x844 (>= (- title_top_right_kid_6_x title_top_right_x) 0.0)))
 (let ((?x840 (+ (- (- title_top_right_kid_5_y) title_top_right_kid_5_hight) title_top_right_y)))
 (let (($x842 (>= (+ ?x840 title_top_right_hight) 0.0)))
 (let (($x837 (>= ?x836 0.0)))
 (let ((?x833 (- (- title_top_right_width title_top_right_kid_5_x) title_top_right_kid_5_width)))
 (let (($x835 (>= (+ ?x833 title_top_right_x) 0.0)))
 (let (($x831 (>= (- title_top_right_kid_5_x title_top_right_x) 0.0)))
 (let ((?x827 (- (+ (- title_top_right_kid_4_y) title_top_right_y) title_top_right_kid_4_hight)))
 (let (($x829 (>= (+ ?x827 title_top_right_hight) 0.0)))
 (let (($x824 (>= ?x823 0.0)))
 (let ((?x820 (+ (- title_top_right_width title_top_right_kid_4_x) title_top_right_x)))
 (let (($x822 (>= (- ?x820 title_top_right_kid_4_width) 0.0)))
 (let (($x818 (>= (- title_top_right_kid_4_x title_top_right_x) 0.0)))
 (let ((?x814 (+ (- title_top_right_y title_top_right_kid_3_y) title_top_right_hight)))
 (let (($x816 (>= (- ?x814 title_top_right_kid_3_hight) 0.0)))
 (let (($x812 (>= ?x811 0.0)))
 (let ((?x808 (+ (- title_top_right_width title_top_right_kid_3_width) title_top_right_x)))
 (let (($x810 (>= (- ?x808 title_top_right_kid_3_x) 0.0)))
 (let (($x806 (>= (+ (- title_top_right_x) title_top_right_kid_3_x) 0.0)))
 (let ((?x801 (- (+ (- title_top_right_kid_2_y) title_top_right_y) title_top_right_kid_2_hight)))
 (let (($x803 (>= (+ ?x801 title_top_right_hight) 0.0)))
 (let (($x798 (>= ?x797 0.0)))
 (let ((?x794 (- (+ (- title_top_right_kid_2_width) title_top_right_width) title_top_right_kid_2_x)))
 (let (($x796 (>= (+ ?x794 title_top_right_x) 0.0)))
 (let (($x791 (>= (- title_top_right_kid_2_x title_top_right_x) 0.0)))
 (let ((?x787 (+ (- title_top_right_y title_top_right_kid_1_y) title_top_right_hight)))
 (let (($x789 (>= (- ?x787 title_top_right_kid_1_hight) 0.0)))
 (let (($x785 (>= ?x784 0.0)))
 (let ((?x781 (- (+ (- title_top_right_kid_1_x) title_top_right_width) title_top_right_kid_1_width)))
 (let (($x783 (>= (+ ?x781 title_top_right_x) 0.0)))
 (let (($x778 (>= (- title_top_right_kid_1_x title_top_right_x) 0.0)))
 (let ((?x774 (+ (+ (- title_top_right_kid_0_hight) title_top_right_y) title_top_right_hight)))
 (let (($x776 (>= (- ?x774 title_top_right_kid_0_y) 0.0)))
 (let (($x771 (>= ?x770 0.0)))
 (let ((?x766 (- (- title_top_right_width title_top_right_kid_0_x) title_top_right_kid_0_width)))
 (let (($x768 (>= (+ ?x766 title_top_right_x) 0.0)))
 (let (($x764 (>= ?x763 0.0)))
 (let (($x762 (>= title_top_right_kid_7_hight 0.0)))
 (let (($x761 (>= title_top_right_kid_7_width 0.0)))
 (let (($x760 (>= title_top_right_kid_7_y 0.0)))
 (let (($x759 (>= title_top_right_kid_7_x 0.0)))
 (let (($x758 (>= title_top_right_kid_6_hight 0.0)))
 (let (($x757 (>= title_top_right_kid_6_width 0.0)))
 (let (($x756 (>= title_top_right_kid_6_y 0.0)))
 (let (($x755 (>= title_top_right_kid_6_x 0.0)))
 (let (($x754 (>= title_top_right_kid_5_hight 0.0)))
 (let (($x753 (>= title_top_right_kid_5_width 0.0)))
 (let (($x752 (>= title_top_right_kid_5_y 0.0)))
 (let (($x751 (>= title_top_right_kid_5_x 0.0)))
 (let (($x750 (>= title_top_right_kid_4_hight 0.0)))
 (let (($x749 (>= title_top_right_kid_4_width 0.0)))
 (let (($x748 (>= title_top_right_kid_4_y 0.0)))
 (let (($x747 (>= title_top_right_kid_4_x 0.0)))
 (let (($x746 (>= title_top_right_kid_3_hight 0.0)))
 (let (($x745 (>= title_top_right_kid_3_width 0.0)))
 (let (($x744 (>= title_top_right_kid_3_y 0.0)))
 (let (($x743 (>= title_top_right_kid_3_x 0.0)))
 (let (($x742 (>= title_top_right_kid_2_hight 0.0)))
 (let (($x741 (>= title_top_right_kid_2_width 0.0)))
 (let (($x740 (>= title_top_right_kid_2_y 0.0)))
 (let (($x739 (>= title_top_right_kid_2_x 0.0)))
 (let (($x738 (>= title_top_right_kid_1_hight 0.0)))
 (let (($x737 (>= title_top_right_kid_1_width 0.0)))
 (let (($x736 (>= title_top_right_kid_1_y 0.0)))
 (let (($x735 (>= title_top_right_kid_1_x 0.0)))
 (let (($x734 (>= title_top_right_kid_0_hight 0.0)))
 (let (($x733 (>= title_top_right_kid_0_width 0.0)))
 (let (($x732 (>= title_top_right_kid_0_y 0.0)))
 (let (($x731 (>= title_top_right_kid_0_x 0.0)))
 (let ((?x728 (- (- title_top_left_kid_2_hight title_top_left_y) title_top_left_hight)))
 (let (($x730 (= (+ ?x728 title_top_left_kid_2_y) 0.0)))
 (let ((?x724 (- (+ title_top_left_kid_1_y title_top_left_kid_1_hight) title_top_left_y)))
 (let (($x726 (= (- ?x724 title_top_left_hight) 0.0)))
 (let ((?x667 (- title_top_left_kid_0_y title_top_left_y)))
 (let (($x722 (= (- (+ ?x667 title_top_left_kid_0_hight) title_top_left_hight) 0.0)))
 (let ((?x694 (+ (- title_top_left_y) title_top_left_kid_2_y)))
 (let (($x719 (= ?x694 0.0)))
 (let ((?x680 (- title_top_left_kid_1_y title_top_left_y)))
 (let (($x718 (= ?x680 0.0)))
 (let (($x717 (= ?x667 0.0)))
 (let ((?x714 (+ (+ (- title_top_left_width) title_top_left_kid_2_x) title_top_left_kid_2_width)))
 (let (($x716 (= (- ?x714 title_top_left_x) 0.0)))
 (let ((?x661 (- title_top_left_kid_0_x title_top_left_x)))
 (let (($x712 (= ?x661 0.0)))
 (let (($x711 (= title_top_left_kid_2_width 100.0)))
 (let (($x710 (= title_top_left_kid_1_width 100.0)))
 (let (($x708 (= title_top_left_kid_0_width 50.0)))
 (let ((?x705 (- (- title_top_left_kid_2_x title_top_left_kid_1_x) title_top_left_kid_1_width)))
 (let (($x706 (>= ?x705 0.0)))
 (let ((?x702 (- (- title_top_left_kid_1_x title_top_left_kid_0_x) title_top_left_kid_0_width)))
 (let (($x703 (>= ?x702 0.0)))
 (let ((?x698 (+ (+ (- title_top_left_kid_2_hight) title_top_left_y) title_top_left_hight)))
 (let (($x700 (>= (- ?x698 title_top_left_kid_2_y) 0.0)))
 (let (($x695 (>= ?x694 0.0)))
 (let ((?x690 (- (- title_top_left_width title_top_left_kid_2_x) title_top_left_kid_2_width)))
 (let (($x692 (>= (+ ?x690 title_top_left_x) 0.0)))
 (let (($x688 (>= (- title_top_left_kid_2_x title_top_left_x) 0.0)))
 (let ((?x684 (+ (- (- title_top_left_kid_1_y) title_top_left_kid_1_hight) title_top_left_y)))
 (let (($x686 (>= (+ ?x684 title_top_left_hight) 0.0)))
 (let (($x681 (>= ?x680 0.0)))
 (let ((?x677 (- (- title_top_left_width title_top_left_kid_1_x) title_top_left_kid_1_width)))
 (let (($x679 (>= (+ ?x677 title_top_left_x) 0.0)))
 (let (($x675 (>= (- title_top_left_kid_1_x title_top_left_x) 0.0)))
 (let ((?x671 (- (+ (- title_top_left_kid_0_y) title_top_left_y) title_top_left_kid_0_hight)))
 (let (($x673 (>= (+ ?x671 title_top_left_hight) 0.0)))
 (let (($x668 (>= ?x667 0.0)))
 (let ((?x665 (- (+ (- title_top_left_width title_top_left_kid_0_x) title_top_left_x) title_top_left_kid_0_width)))
 (let (($x666 (>= ?x665 0.0)))
 (let (($x662 (>= ?x661 0.0)))
 (let (($x660 (>= title_top_left_kid_2_hight 0.0)))
 (let (($x659 (>= title_top_left_kid_2_width 0.0)))
 (let (($x658 (>= title_top_left_kid_2_y 0.0)))
 (let (($x657 (>= title_top_left_kid_2_x 0.0)))
 (let (($x656 (>= title_top_left_kid_1_hight 0.0)))
 (let (($x655 (>= title_top_left_kid_1_width 0.0)))
 (let (($x654 (>= title_top_left_kid_1_y 0.0)))
 (let (($x653 (>= title_top_left_kid_1_x 0.0)))
 (let (($x652 (>= title_top_left_kid_0_hight 0.0)))
 (let (($x651 (>= title_top_left_kid_0_width 0.0)))
 (let (($x650 (>= title_top_left_kid_0_y 0.0)))
 (let (($x649 (>= title_top_left_kid_0_x 0.0)))
 (let ((?x552 (- title_top_x title_bg_x)))
 (let (($x553 (= ?x552 0.0)))
 (let ((?x647 (- (+ (+ (- title_top_hight) title_top_right_y) title_top_right_hight) title_top_y)))
 (let (($x648 (= ?x647 0.0)))
 (let ((?x628 (- title_top_right_y title_top_y)))
 (let (($x644 (= ?x628 0.0)))
 (let ((?x642 (- (+ (+ (- title_top_hight) title_top_left_y) title_top_left_hight) title_top_y)))
 (let (($x643 (= ?x642 0.0)))
 (let ((?x615 (- title_top_left_y title_top_y)))
 (let (($x639 (= ?x615 0.0)))
 (let (($x638 (= title_top_hight 40.0)))
 (let (($x636 (>= (+ (- (- title_top_left_width) title_top_left_x) title_top_right_x) 0.0)))
 (let ((?x632 (+ (- (- title_top_hight title_top_right_y) title_top_right_hight) title_top_y)))
 (let (($x633 (>= ?x632 0.0)))
 (let (($x629 (>= ?x628 0.0)))
 (let ((?x626 (- (+ (+ (- title_top_right_width) title_top_x) title_top_width) title_top_right_x)))
 (let (($x627 (>= ?x626 0.0)))
 (let (($x622 (>= (+ ?x570 title_top_right_x) 0.0)))
 (let ((?x619 (+ (- (- title_top_hight title_top_left_y) title_top_left_hight) title_top_y)))
 (let (($x620 (>= ?x619 0.0)))
 (let (($x616 (>= ?x615 0.0)))
 (let ((?x613 (- (+ (+ (- title_top_left_width) title_top_x) title_top_width) title_top_left_x)))
 (let (($x614 (>= ?x613 0.0)))
 (let (($x609 (>= ?x608 0.0)))
 (let (($x607 (>= title_top_right_hight 0.0)))
 (let (($x606 (>= title_top_right_width 0.0)))
 (let (($x605 (>= title_top_right_y 0.0)))
 (let (($x604 (>= title_top_right_x 0.0)))
 (let (($x603 (>= title_top_left_hight 0.0)))
 (let (($x602 (>= title_top_left_width 0.0)))
 (let (($x601 (>= title_top_left_y 0.0)))
 (let (($x600 (>= title_top_left_x 0.0)))
 (let ((?x518 (- title_bg_y back_ground_y)))
 (let (($x599 (= ?x518 0.0)))
 (let ((?x597 (+ (- (+ (- back_ground_width) title_bg_x) back_ground_x) title_bg_width)))
 (let (($x598 (= ?x597 0.0)))
 (let ((?x512 (- title_bg_x back_ground_x)))
 (let (($x593 (= ?x512 0.0)))
 (let ((?x550 (- (+ (- title_top_hight) title_bar_y) title_top_y)))
 (let (($x592 (>= ?x550 0.0)))
 (let (($x591 (>= (- (- (+ title_bg_y title_bg_hight) title_bar_y) title_bar_hight) 0.0)))
 (let (($x587 (>= (+ (- title_bg_y) title_bar_y) 0.0)))
 (let ((?x584 (+ (+ (- (- title_bar_x) title_bar_width) title_bg_x) title_bg_width)))
 (let (($x585 (>= ?x584 0.0)))
 (let (($x580 (>= ?x554 0.0)))
 (let (($x579 (>= (- (+ (- title_bg_y title_top_hight) title_bg_hight) title_top_y) 0.0)))
 (let ((?x501 (- title_bg_y)))
 (let ((?x563 (+ ?x501 title_top_y)))
 (let (($x575 (>= ?x563 0.0)))
 (let (($x574 (>= (+ (- (+ ?x570 title_bg_x) title_top_width) title_bg_width) 0.0)))
 (let (($x569 (>= ?x552 0.0)))
 (let (($x568 (= (+ (+ (- ?x501 title_bg_hight) title_bar_y) title_bar_hight) 0.0)))
 (let (($x564 (= ?x563 0.0)))
 (let (($x562 (= (- (- (+ title_bar_x title_bar_width) title_bg_x) title_bg_width) 0.0)))
 (let (($x558 (= (- (+ ?x552 title_top_width) title_bg_width) 0.0)))
 (let (($x551 (= ?x550 0.0)))
 (let (($x547 (>= title_bar_hight 0.0)))
 (let (($x546 (>= title_bar_width 0.0)))
 (let (($x545 (>= title_bar_y 0.0)))
 (let (($x544 (>= title_bar_x 0.0)))
 (let (($x543 (>= title_top_hight 0.0)))
 (let (($x542 (>= title_top_width 0.0)))
 (let (($x541 (>= title_top_y 0.0)))
 (let (($x540 (>= title_top_x 0.0)))
 (let (($x539 (= (- back_ground_y BC_y) 0.0)))
 (let ((?x503 (- (+ ?x501 main_body_y) title_bg_hight)))
 (let (($x537 (>= ?x503 0.0)))
 (let ((?x535 (+ (- (+ (- main_body_y) back_ground_y) main_body_hight) back_ground_hight)))
 (let (($x536 (>= ?x535 0.0)))
 (let (($x531 (>= (- main_body_y back_ground_y) 0.0)))
 (let ((?x528 (- (+ (- back_ground_width main_body_x) back_ground_x) main_body_width)))
 (let (($x529 (>= ?x528 0.0)))
 (let (($x525 (>= (- main_body_x back_ground_x) 0.0)))
 (let (($x523 (>= (+ (- (+ ?x501 back_ground_y) title_bg_hight) back_ground_hight) 0.0)))
 (let (($x519 (>= ?x518 0.0)))
 (let ((?x516 (- (+ (- back_ground_width title_bg_x) back_ground_x) title_bg_width)))
 (let (($x517 (>= ?x516 0.0)))
 (let (($x513 (>= ?x512 0.0)))
 (let (($x511 (= (- (+ (- back_ground_width BC_width) back_ground_x) BC_x) 0.0)))
 (let (($x507 (= (- back_ground_x BC_x) 0.0)))
 (let (($x505 (= ?x503 20.0)))
 (let (($x500 (>= main_body_hight 0.0)))
 (let (($x499 (>= main_body_width 0.0)))
 (let (($x498 (>= main_body_y 0.0)))
 (let (($x497 (>= main_body_x 0.0)))
 (let (($x496 (>= title_bg_hight 0.0)))
 (let (($x495 (>= title_bg_width 0.0)))
 (let (($x494 (>= title_bg_y 0.0)))
 (let (($x493 (>= title_bg_x 0.0)))
 (let (($x492 (>= back_ground_hight 0.0)))
 (let (($x491 (>= back_ground_width 0.0)))
 (let (($x490 (>= back_ground_y 0.0)))
 (let (($x489 (>= back_ground_x 0.0)))
 (let (($x488 (= BC_y 0.0)))
 (let (($x487 (= BC_x 0.0)))
 (let (($x486 (<= BC_width 4000.0)))
 (let (($x484 (>= BC_hight 0.0)))
 (let (($x483 (>= BC_width 0.0)))
 (let (($x482 (>= BC_y 0.0)))
 (let (($x481 (>= BC_x 0.0)))
 (and $x481 $x482 $x483 $x484 $x486 $x487 $x488 BC_feasible $x489 $x490 $x491 $x492 $x493 $x494 $x495 $x496 $x497 $x498 $x499 $x500 $x505 $x507 $x511 $x513 $x517 $x519 $x523 $x525 $x529 $x531 $x536 $x537 $x539 $x540 $x541 $x542 $x543 $x544 $x545 $x546 $x547 $x551 $x553 $x555 $x558 $x562 $x564 $x568 $x569 $x574 $x575 $x579 $x580 $x585 $x587 $x591 $x592 $x593 $x598 $x599 $x600 $x601 $x602 $x603 $x604 $x605 $x606 $x607 $x609 $x614 $x616 $x620 $x622 $x627 $x629 $x633 $x636 $x638 $x639 $x643 $x644 $x648 $x553 $x649 $x650 $x651 $x652 $x653 $x654 $x655 $x656 $x657 $x658 $x659 $x660 $x662 $x666 $x668 $x673 $x675 $x679 $x681 $x686 $x688 $x692 $x695 $x700 $x703 $x706 $x708 $x710 $x711 $x712 $x716 $x717 $x718 $x719 $x722 $x726 $x730 $x731 $x732 $x733 $x734 $x735 $x736 $x737 $x738 $x739 $x740 $x741 $x742 $x743 $x744 $x745 $x746 $x747 $x748 $x749 $x750 $x751 $x752 $x753 $x754 $x755 $x756 $x757 $x758 $x759 $x760 $x761 $x762 $x764 $x768 $x771 $x776 $x778 $x783 $x785 $x789 $x791 $x796 $x798 $x803 $x806 $x810 $x812 $x816 $x818 $x822 $x824 $x829 $x831 $x835 $x837 $x842 $x844 $x848 $x850 $x855 $x857 $x861 $x863 $x868 $x871 $x874 $x877 $x881 $x884 $x887 $x891 $x894 $x896 $x898 $x900 $x902 $x904 $x906 $x907 $x908 $x912 $x913 $x914 $x915 $x916 $x917 $x918 $x919 $x920 $x924 $x927 $x930 $x933 $x936 $x940 $x944 $x948 $x949 $x950 $x951 $x952 $x953 $x954 $x955 $x956 $x960 $x961 $x962 $x963 $x964 $x965 $x966 $x967 $x968 $x970 $x975 $x977 $x982 $x984 $x989 $x991 $x996 $x999 $x1001 $x555 $x1002 $x1005 $x1008 $x1015 $x1016 $x1017 $x1018 $x1019 $x1020 $x1021 $x1022 $x1023 $x1024 $x1025 $x1026 $x1027 $x1028 $x1029 $x1030 $x1031 $x1032 $x1033 $x1034 $x1035 $x1036 $x1037 $x1038 $x1039 $x1040 $x1043 $x1047 $x1049 $x1053 $x1055 $x1059 $x1061 $x1066 $x1068 $x1072 $x1074 $x1079 $x1081 $x1085 $x1087 $x1092 $x1094 $x1098 $x1100 $x1105 $x1107 $x1111 $x1113 $x1117 $x1121 $x1124 $x1127 $x1131 $x1135 $x1137 $x1139 $x1141 $x1143 $x1145 $x1146 $x1149 $x1152 $x1154 $x1156 $x1158 $x1160 $x1162 $x1167 $x1168 $x1169 $x1170 $x1171 $x1172 $x1173 $x1176 $x1179 $x1183 $x1187 $x1191 $x1194 $x1195 $x1196 $x1197 $x1198 $x1199 $x1203 $x1204 $x1205 $x1206 $x1207 $x1214 $x1220 $x1223 $x1226 $x1227 $x1228 $x1229 $x1230 $x1232 $x1234 $x1237 $x1239 $x1240 $x1241 $x1242 $x1243 $x1246 $x1249 $x1253 $x1255 $x1256 $x1257 $x1258 $x1259 $x1260 $x1261 $x1262 $x1263 $x1266 $x1270 $x1272 $x1277 $x1279 $x1284 $x1286 $x1290 $x1293 $x1294 $x1295 $x1298 $x1301 $x1302 $x1306 $x1312 $x1317 $x1320 $x1321 $x1322 $x1323 $x1324 $x1325 $x1326 $x1327 $x1328 $x1332 $x1336 $x1339 $x1344 $x1349 $x1354 $x1357 $x1361 $x1362 $x1363 $x1364 $x1365 $x1366 $x1367 $x1368 $x1369 $x1370 $x1371 $x1372 $x1373 $x1374 $x1375 $x1379 $x1385 $x1388 $x1393 $x1396 $x1402 $x1405 $x1410 $x1413 $x1418 $x1421 $x1426 $x1430 $x1434 $x1436 $x1438 $x1440 $x1445 $x1447 $x1449 $x1451 $x1457 $x1462 $x1467 $x1470 $x1472 $x1473 $x1474 $x1475 $x1476 $x1477 $x1478 $x1479 $x1480 $x1481 $x1482 $x1483 $x1484 $x1485 $x1486 $x1487 $x1488 $x1494 $x1499 $x1503 $x1506 $x1509 $x1512 $x1516 $x1520 $x1525 $x1530 $x1535 $x1539 $x1544 $x1546 $x1552 $x1554 $x1559 $x1561 $x1567 $x1570 $x1575 $x1577 $x1583 $x1586 $x1590 $x1592 $x1598 $x1601 $x1605 $x1607 $x1609 $x1611 $x1614 $x1617 $x1620 $x1623 $x1626 $x1627 $x1628 $x1629 $x1630 $x1631 $x1632 $x1633 $x1634 $x1635 $x1636 $x1637 $x1638 $x1643 $x1647 $x1650 $x1655 $x1658 $x1663 $x1666 $x1671 $x1674 $x1680 $x1683 $x1687 $x1690 $x1695 $x1699 $x1703 $x1705 $x1710 $x1712 $x1714 $x1716 $x1721 $x1726 $x1731 $x1733 $x1735 $x1736 $x1737 $x1738 $x1739 $x1740 $x1741 $x1742 $x1743 $x1744 $x1745 $x1746 $x1747 $x1748 $x1749 $x1750 $x1751 $x1752 $x1753 $x1754 $x1755 $x1756 $x1757 $x1758 $x1759 $x1763 $x1767 $x1770 $x1776 $x1779 $x1784 $x1787 $x1792 $x1795 $x1800 $x1803 $x1809 $x1812 $x1817 $x1820 $x1826 $x1829 $x1833 $x1836 $x1842 $x1845 $x1849 $x1852 $x1858 $x1862 $x1867 $x1872 $x1877 $x1881 $x1883 $x1887 $x1889 $x1891 $x1893 $x1895 $x1897 $x1899 $x1904 $x1908 $x1913 $x1917 $x1922 $x1927 $x1929 $x1931 $x1933 $x1935 $x1937 $x1939 $x1941 $x1944 $x1946 $x1948 $x1955 $x1962 $x1969 $x1976 $x1977 $x1978 $x1979 $x1980 $x1981 $x1982 $x1983 $x1984 $x1985 $x1986 $x1987 $x1988 $x1989 $x1990 $x1991 $x1992 $x1993 $x1994 $x1995 $x1996 $x1997 $x1998 $x1999 $x2000 $x2004 $x2008 $x2011 $x2017 $x2020 $x2025 $x2029 $x2035 $x2038 $x2044 $x2047 $x2053 $x2056 $x2062 $x2065 $x2071 $x2074 $x2080 $x2083 $x2089 $x2092 $x2096 $x2099 $x2105 $x2109 $x2113 $x2117 $x2121 $x2125 $x2127 $x2131 $x2133 $x2135 $x2137 $x2139 $x2141 $x2143 $x2148 $x2153 $x2157 $x2161 $x2166 $x2171 $x2173 $x2175 $x2177 $x2179 $x2181 $x2183 $x2185 $x2188 $x2191 $x2193 $x2200 $x2206 $x2213 $x2220 $x2221 $x2222 $x2223 $x2224 $x2225 $x2226 $x2227 $x2228 $x2229 $x2230 $x2231 $x2232 $x2233 $x2234 $x2235 $x2236 $x2237 $x2238 $x2239 $x2240 $x2244 $x2247 $x2252 $x2258 $x2261 $x2265 $x2268 $x2272 $x2275 $x2278 $x2281 $x2284 $x2290 $x2295 $x2300 $x2305 $x2308 $x2312 $x2316 $x2320 $x2323 $x2328 $x2331 $x2337 $x2340 $x2345 $x2348 $x2352 $x2353 $x2356 $x2361 $x2369 $x2371 $x2375 $x2377 $x2381 $x2382 $x2383 $x2384 $x2385 $x2386 $x2387 $x2388 $x2389 $x2390 $x2391 $x2392 $x2393 $x2396 $x2399 $x2401 $x2406 $x2408 $x2412 $x2414 $x2418 $x2420 $x2425 $x2427 $x2431 $x2433 $x2438 $x2439 $x2440 $x2442 $x2444 $x2450 $x2451 $x2452 $x2453 $x2454 $x2455 $x2456 $x2457 $x2458 $x2459 $x2460 $x2461 $x2462 $x2463 $x2464 $x2465 $x2466 $x2467 $x2468 $x2469 $x2470 $x2471 $x2472 $x2473 $x2474 $x2475 $x2477 $x2481 $x2483 $x2485 $x2487 $x2489 $x2491 $x2493 $x2496 $x2500 $x2504 $x2507 $x2510 $x2513 $x2514 $x2519 $x2520 $x2525 $x2527 $x2532 $x2533 $x2538 $x2541 $x2546 $x2547 $x2551 $x2553 $x2558 $x2559 $x2562 $x2564 $x2569 $x2570 $x2574 $x2575 $x2580 $x2581 $x2586 $x2589 $x2591 $x2594 $x2597 $x2600 $x2601 $x2605 $x2606 $x2609 $x2611 $x2613 $x2615 $x2617 $x2618 $x2619 $x2620 $x2621 $x2622 $x2623 $x2624 $x2625 $x2626 $x2627 $x2628 $x2629 $x2630 $x2631 $x2632 $x2633 $x2634 $x2635 $x2636 $x2637 $x2638 $x2639 $x2640 $x2641 $x2642 $x2643 $x2644 $x2645 $x2646 $x2647 $x2648 $x2649 $x2650 $x2651 $x2652 $x2653 $x2654 $x2655 $x2656 $x2657 $x2658 $x2659 $x2660 $x2661 $x2662 $x2663 $x2664 $x2665 $x2666 $x2667 $x2668 $x2669 $x2670 $x2671 $x2672 $x2673 $x2674 $x2675 $x2676 $x2677 $x2678 $x2679 $x2680 $x2681 $x2682 $x2683 $x2684 $x2685 $x2686 $x2687 $x2688 $x2689 $x2690 $x2691 $x2692 $x2693 $x2694 $x2695 $x2696 $x2697 $x2698 $x2699 $x2700 $x2701 $x2702 $x2703 $x2704 $x2705 $x2706 $x2707 $x2708 $x2709 $x2710 $x2711 $x2712 $x2713 $x2714 $x2715 $x2716 $x2717 $x2718 $x2719 $x2720 $x2721 $x2722 $x2723 $x2726 $x2728 $x2730 $x2734 $x2738 $x2741 $x2743 $x2746 $x2749 $x2752 $x2754 $x2757 $x2759 $x2762 $x2765 $x2767 $x2770 $x2772 $x2775 $x2777 $x2780 $x2783 $x2785 $x2788 $x2791 $x2794 $x2797 $x2799 $x2802 $x2804 $x2807 $x2809 $x2811 $x2813 $x2815 $x2817 $x2819 $x2821 $x2824 $x2826 $x2829 $x2831 $x2833 $x2835 $x2837 $x2839 $x2842 $x2844 $x2847 $x2849 $x2851 $x2853 $x2855 $x2857 $x2859 $x2861 $x2864 $x2867 $x2870 $x2873 $x2876 $x2878 $x2880 $x2882 $x2884 $x2886 $x2889 $x2892 $x2894 $x2896 $x2898 $x2900 $x2902 $x2904 $x2906 $x2908 $x2910 $x2913 $x2915 $x2918 $x2920 $x2923 $x2925 $x2927 $x2930 $x2934 $x2938 $x2942 $x2946 $x2950 $x2954 $x2958 $x2962 $x2964 $x2966 $x2968 $x2970 $x2972 $x2975 $x2978 $x2981 $x2987 $x2991 $x2995 $x3000 $x3004 $x3008 $x3012 $x3016 $x3020 $x3024 $x3028 $x3032 $x3036 $x3040 $x3044 $x3048 $x3052 $x3056 $x3060 $x3064 $x3068 $x3072 $x3076 $x3080 $x3084 back_ground_feasible title_bg_feasible main_body_feasible title_top_feasible title_bar_feasible title_top_left_feasible title_top_right_feasible title_top_left_kid_0_feasible title_top_left_kid_1_feasible title_top_left_kid_2_feasible title_top_right_kid_0_feasible title_top_right_kid_1_feasible title_top_right_kid_2_feasible title_top_right_kid_3_feasible title_top_right_kid_4_feasible title_top_right_kid_5_feasible title_top_right_kid_6_feasible title_top_right_kid_7_feasible icon_feasible search_buttons_feasible search_buttons_kid_0_feasible search_buttons_kid_1_feasible search_buttons_kid_2_feasible search_buttons_kid_3_feasible search_buttons_kid_4_feasible search_buttons_kid_5_feasible search_box_feasible search_icon_feasible cart_feasible ads_holder_feasible recommend_feasible $x3086 $x3087 $x3088 $x3089 $x3091 $x3092 $x3093 $x3094 $x3095 $x3096 $x3097 $x3098 $x3099 $x3100 $x3101 $x3102 $x3103 $x3104 $x3106 $x3107 $x3109 $x3110 $x3112 $x3113 $x3115 $x3116 $x3118 $x3119 $x3121 $x3122 $x3124 $x3125 $x3127 $x3128 $x3130 $x3131 $x3133 $x3134 $x3136 $x3137 $x3139 $x3140 $x3142 $x3143 $x3145 $x3146 $x3148 $x3149 $x3151 $x3152 $x3154 $x3155 $x3157 $x3158 $x3160 $x3161 $x3163 $x3164 rec_title_feasible select_feasible rec_tbl_feasible select_kid_0_feasible select_kid_1_feasible select_kid_2_feasible select_kid_3_feasible select_kid_4_feasible select_kid_5_feasible rec_tbl_kid_0_feasible rec_tbl_kid_1_feasible rec_tbl_kid_2_feasible rec_tbl_kid_3_feasible rec_tbl_kid_4_feasible rec_tbl_kid_5_feasible rec_tbl_kid_6_feasible rec_tbl_kid_7_feasible rec_tbl_kid_8_feasible rec_tbl_kid_9_feasible rec_tbl_kid_10_feasible rec_tbl_kid_11_feasible rec_tbl_kid_12_feasible rec_tbl_kid_13_feasible rec_tbl_kid_14_feasible rec_tbl_kid_15_feasible rec_tbl_kid_16_feasible rec_tbl_kid_17_feasible rec_tbl_kid_18_feasible rec_tbl_kid_19_feasible rec_tbl_kid_20_feasible rec_tbl_kid_21_feasible rec_tbl_kid_22_feasible rec_tbl_kid_23_feasible rec_tbl_kid_24_feasible)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

